Commit 2023-05-20 19:38 fae93aa3

View on Github →

feat: port Analysis.NormedSpace.MazurUlam (#4145)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/MazurUlam.lean

added theorem IsometryEquiv.coeFn_toRealAffineIsometryEquiv

added theorem IsometryEquiv.coe_toRealAffineIsometryEquiv

added theorem IsometryEquiv.coe_to_real_linear_equiv_of_map_zero

added theorem IsometryEquiv.coe_to_real_linear_equiv_of_map_zero_symm

added theorem IsometryEquiv.map_midpoint

added theorem IsometryEquiv.midpoint_fixed

added def IsometryEquiv.toRealAffineIsometryEquiv

added def IsometryEquiv.toRealLinearIsometryEquiv

added def IsometryEquiv.toRealLinearIsometryEquivOfMapZero

added theorem IsometryEquiv.toRealLinearIsometryEquiv_symm_apply

added theorem IsometryEquiv.to_real_linear_equiv_apply