Commit 2022-07-21 02:26 34d4a9bf

View on Github →

feat(analysis/normed_space/linear_isometry): linear_equiv.of_eq as a linear_isometry_equiv (#15471) We also setup simps on linear_isometry and linear_isometry_equiv.

Estimated changes

Modified src/analysis/normed_space/linear_isometry.lean

added def linear_isometry.simps.apply

added theorem linear_isometry_equiv.coe_of_eq_apply

added def linear_isometry_equiv.of_eq

added theorem linear_isometry_equiv.of_eq_rfl

added theorem linear_isometry_equiv.of_eq_symm

added def linear_isometry_equiv.simps.apply

added def linear_isometry_equiv.simps.symm_apply

Modified src/linear_algebra/basic.lean

added theorem linear_equiv.of_eq_rfl