Theorem Homogenization.hom_ext_iff

Modification history

2026-09-07 15:38

Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean

feat(LinearAlgebra/AffineSpace/Homogenization): generalize `hom_ext` to `LinearMapClass` (#43350)

Modified Homogenization.hom_ext_iff View on Github →

2026-08-31 10:08

Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean

feat: homogenization of an affine space (#39368)

Added Homogenization.hom_ext_iff View on Github →