Commit 2025-11-16 20:03 2536bec5

View on Github →

chore: rename foo_of_norm_one to foo_of_norm_eq_one (#31674) These should be called foo_of_norm_eq_one and not foo_of_norm_one. We already have two lemmas that are correctly named this way: NormedSpace.normalize_eq_self_of_norm_eq_one and NumberField.Embeddings.pow_eq_one_of_norm_eq_one.

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean

Modified Mathlib/Analysis/Complex/Norm.lean

added theorem Complex.norm_sub_one_sq_eq_of_norm_eq_one

deleted theorem Complex.norm_sub_one_sq_eq_of_norm_one

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem inner_eq_one_iff_of_norm_eq_one

deleted theorem inner_eq_one_iff_of_norm_one

added theorem inner_lt_one_iff_real_of_norm_eq_one

deleted theorem inner_lt_one_iff_real_of_norm_one

added theorem inner_self_eq_one_of_norm_eq_one

deleted theorem inner_self_eq_one_of_norm_one

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

added theorem Seminorm.map_eq_zero_of_norm_eq_zero

deleted theorem Seminorm.map_eq_zero_of_norm_zero

Modified Mathlib/Analysis/Normed/Operator/Basic.lean

added theorem norm_image_of_norm_eq_zero

deleted theorem norm_image_of_norm_zero

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

added theorem NumberField.mixedEmbedding.logMap_apply_of_norm_eq_one

deleted theorem NumberField.mixedEmbedding.logMap_apply_of_norm_one