Commit 2026-08-31 10:08 29cc1eef

View on Github →

feat: homogenization of an affine space (#39368)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean

added theorem Homogenization.coe_congr

added theorem Homogenization.coe_liftₗ

added theorem Homogenization.coe_liftₗ_symm

added def Homogenization.congr

added theorem Homogenization.congr_eq_refl_iff

added theorem Homogenization.congr_refl

added theorem Homogenization.congr_symm

added theorem Homogenization.congr_trans

added def Homogenization.equivProdAux

added theorem Homogenization.hom_ext

added theorem Homogenization.hom_ext_iff

added theorem Homogenization.induction_of_point

added theorem Homogenization.induction_on

added def Homogenization.lift

added theorem Homogenization.lift_apply_ofPoint

added theorem Homogenization.lift_apply_ofVector

added theorem Homogenization.lift_const_apply

added theorem Homogenization.lift_map

added theorem Homogenization.lift_ofPoint

added theorem Homogenization.lift_smul

added theorem Homogenization.lift_symm_apply

added theorem Homogenization.lift_symm_id

added theorem Homogenization.lift_symm_linear_apply

added theorem Homogenization.lift_symm_smul

added def Homogenization.liftₗ

added def Homogenization.map

added theorem Homogenization.map_apply_ofPoint

added theorem Homogenization.map_apply_ofVector

added theorem Homogenization.map_comp

added theorem Homogenization.map_eq_id_iff

added theorem Homogenization.map_id

added theorem Homogenization.map_injective'

added theorem Homogenization.map_injective

added theorem Homogenization.map_surjective

added def Homogenization.ofPoint

added theorem Homogenization.ofPoint_injective

added theorem Homogenization.ofPoint_linear

added def Homogenization.ofVector

added theorem Homogenization.ofVector_injective

added theorem Homogenization.ofVector_ofPoint_cases

added theorem Homogenization.ofVector_smul

added theorem Homogenization.ofVector_vsub

added theorem Homogenization.span_range_ofPoint

added theorem Homogenization.toLinearMap_congr

added def Homogenization.toProd

added theorem Homogenization.toProd_ofPoint

added theorem Homogenization.toProd_ofVector

added def Homogenization.weight

added theorem Homogenization.weight_eq_one_iff

added theorem Homogenization.weight_eq_zero_iff

added theorem Homogenization.weight_map

added theorem Homogenization.weight_ofPoint

added theorem Homogenization.weight_ofVector

added theorem Homogenization.weight_surjective

added def Homogenization

Modified docs/references.bib