Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-06 20:56 2a36d256

View on Github →

chore(analysis/normed_space/mazur_ulam): add to_affine_map (#2963)

Estimated changes

Modified src/analysis/normed_space/mazur_ulam.lean

added theorem isometric.coe_to_affine_map

added def isometric.to_affine_map

Modified src/linear_algebra/affine_space.lean

added theorem affine_map.coe_mk'

added def affine_map.mk'

added theorem affine_map.mk'_linear