Theorem ContinuousAffineEquiv.toContinuousAffineMap_injective

Modification history

2025-04-25 00:52

Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

feat(LinearAlgebra/AffineSpace/ContinuousAffineEquiv): `toContinuousAffineMap` (#23732) …

Added ContinuousAffineEquiv.toContinuousAffineMap_injective View on Github →