Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.reflection_fixed_iff_of_bit0_inj

Modification history

2020-05-12 15:37

src/data/equiv/mul_add.lean

feat(analysis/normed_space): add Mazur-Ulam theorem (#2214) …

Deleted equiv.reflection_fixed_iff_of_bit0_inj View on Github →

2020-05-07 10:25

src/data/equiv/mul_add.lean

feat(*): define `equiv.reflection` and `isometry.reflection` (#2609) …

Added equiv.reflection_fixed_iff_of_bit0_inj View on Github →