Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_affine_map.coe_injective

Modification history

2023-03-13 22:49
src/topology/algebra/continuous_affine_map.lean
refactor(linear_algebra/affine_space/affine_{map,equiv}): add fun_like instances (#18575) …
Modified continuous_affine_map.coe_injectiveView on Github →
2021-11-06 20:27
src/topology/algebra/continuous_affine_map.lean
feat(analysis/normed_space/continuous_affine_map): define bundled continuous affine maps (#10161) …
Added continuous_affine_map.coe_injectiveView on Github →