Commit 2026-06-03 23:05 97f12126

View on Github →

feat(LinearAlgebra/AffineSpace/AffineSubspace): using AffineSubspace.direction to reinterpret AffineSubspace as Submodule (#38731)

  • add AffineSubspace.vsub_self_of_zero_mem that states s -ᵥ s = s if 0 ∈ s
  • add AffineSubspace.direction_eq_self_iff_zero_mem that states that 0 ∈ s iff the directions coerce back to the affine subspace.
  • add corresponding CanLift instance.
  • modify doc-string of AffineSubspace.direction to state that this can be used for reinterpretation of an affine subspace as a submodule.
  • add Coe instance based on Submodule.toAffineSubspace and adds corresponding @[coe] attribute. The PR also performs a slight cleanup of the file: statements about SetLike or Submodule.toAffineSubspace have been moved closer to their respective definitions. Because the PR was temporarily broken, I also added
  • the lemma carrier_eq_coe (s : AffineSubspace k P) : s.carrier = s

Estimated changes