Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_isometry_equiv.of_eq_rfl

Modification history

2022-07-21 02:26

src/analysis/normed_space/linear_isometry.lean

feat(analysis/normed_space/linear_isometry): `linear_equiv.of_eq` as a `linear_isometry_equiv` (#15471) …

Added linear_isometry_equiv.of_eq_rfl View on Github →