OAI/Geometry/Convex/GeneralMahler/FormSquare.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

§04 profile quadratic identity.

  1. lemma OAI.GeneralMahler.ProjField.tw_add line 15
  2. lemma OAI.GeneralMahler.ProjField.evId line 23
  3. lemma OAI.GeneralMahler.ProjField.Pb_sq line 27
  4. lemma OAI.GeneralMahler.ProjField.form_sq line 33