Commit 2023-05-26 12:43 0b812671

View on Github →

feat: port Analysis.Calculus.Conformal.InnerProduct (#4389)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Conformal/InnerProduct.lean

added theorem conformalAt_iff'

added theorem conformalAt_iff

added def conformalFactorAt

added theorem conformalFactorAt_inner_eq_mul_inner'

added theorem conformalFactorAt_inner_eq_mul_inner

added theorem conformalFactorAt_pos