Commit 2024-02-13 12:46 74925360

View on Github →

chore(AffineIsometry): weaken some Normed* to Seminormed* (#10448)

  • Reorder variables so that related variables are declared on the same line;
  • Use Seminormed*/PseudoMetric* for all non-primed type variables.
  • Introduce V₁'/P₁' for a normed add torsor.

Estimated changes

modified theorem AffineIsometry.map_eq_iff
modified theorem AffineIsometry.map_ne