search

dannypsnl / blackboard

Do random math in Lean.
0 stars 0 forks source link

about isometry #3

Closed dannypsnl closed 2 months ago

dannypsnl commented 2 months ago

2

dannypsnl commented 2 months ago

According to current status of mathlib4 such that Riemann manifold is unsupported yet, no standard way to talk about inner product of tangent space, postpone this idea for a while.