Repository navigation

Defining `IsHomogenization` as linear equivalence - #102

Open

ooovi wants to merge 25 commits into

mainfrom

homogenization_linequiv

Commits on Sep 9, 2026
- making IsHomogenization a struct
  ooovi
  committed
  f1bb7d6
- Merge remote-tracking branch 'origin/main' into homogenization_struct
  ooovi
  committed
  0c65f69
- making a fancy H
  ooovi
  committed
  895aa0f
Commits on Sep 15, 2026
- forgot one
  ooovi
  committed
  3b4ddd2
Commits on Sep 17, 2026
- trying out new definition of homogenization
  ooovi
  committed
  c19e5ef
- addin two little lemmas
  ooovi
  committed
  8e21608
Commits on Sep 28, 2026
- Merge branch 'main' into homogenization_linequiv
  ooovi
  authored
  264098d
Commits on Sep 29, 2026
- cleanup
  ooovi
  committed
  e7804a7
- making it like draft PR
  ooovi
  committed
  635aa70
- some suggestions
  ooovi
  committed
  52c1545
Commits on Sep 30, 2026
- adding constructor for field and nonzero functional
  ooovi
  committed
  c829e9b
- renaming face homogenizaIso
  ooovi
  committed
  e668af4
Commits on Oct 6, 2026
- inlining nonempty proofs
  ooovi
  committed
  90a36cd
- making arg implicit
  ooovi
  committed
  bd4e935
- re-renaming to canonical
  ooovi
  committed
  d6c5f29
- using AffineMap.range
  ooovi
  committed
  7950d7e
- using h for hypothesis
  ooovi
  committed
  0e8ef0a
- Update Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/IsHomogenization.lean
  
  ooovi
  and
  martinwintermath
  authored
  81ddc45
Commits on Oct 7, 2026
- removing non-simple simps
  ooovi
  authored
  19fb7cd
- renaming ofEmbed to ofWeightEmbed
  ooovi
  committed
  49d1d18
- typo
  ooovi
  committed
  9b66d86
Commits on Oct 9, 2026
- own lemma for nonempty
  ooovi
  committed
  6a0aff8
- using AffineMap.range
  ooovi
  committed
  254e0a3
- using range
  ooovi
  committed
  0678828
- fix
  ooovi
  committed
  b7de21f