Commit 2025-04-01 08:25 5e033aa7

View on Github →

chore(LinearAlgebra/AffineSpace): process porting notes (#23505)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

modified theorem AffineEquiv.apply_eq_iff_eq

modified theorem AffineEquiv.coeFn_inj

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

modified theorem AffineSubspace.mem_coe

Modified Mathlib/LinearAlgebra/AffineSpace/Basis.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Matrix.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Restrict.lean