Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-08 00:30 fa3b6222

View on Github →

refactor(analysis/normed_space/linear_isometry): semilinear isometries (#9551) Generalize the theory of linear isometries to the semilinear setting.

Estimated changes

modified theorem linear_isometry.coe_comp
modified def linear_isometry.comp
modified theorem linear_isometry.comp_assoc
modified theorem linear_isometry.ext
modified theorem linear_isometry.id_comp
modified theorem linear_isometry.map_eq_iff
modified theorem linear_isometry.map_ne
modified theorem linear_isometry.map_smul
modified structure linear_isometry
modified theorem linear_isometry_equiv.ext
modified structure linear_isometry_equiv