OAI/Geometry/Convex/GeneralMahler/Linear/Eq25.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Linear field: normalization substitution.

  1. lemma OAI.GeneralMahler.pj_outer line 11
  2. lemma OAI.GeneralMahler.Eq_replace line 18
  3. lemma OAI.GeneralMahler.pairGap line 38
  4. lemma OAI.GeneralMahler.ProjField.eq25 line 52