Def Homogenization.equivProdAux

Modification history

2026-10-17 11:31

Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean

chore(LinearAlgebra/AffineSpace/Homogenization): use `inferInstanceAs` (#44947) …

Deleted Homogenization.equivProdAux View on Github →

2026-08-31 10:08

Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean

feat: homogenization of an affine space (#39368)

Added Homogenization.equivProdAux View on Github →