OAI/NumberTheory/PiExponent/LocalAlgebra/TensorIdealInclusion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Geometry.tensorUnitTwist line 13
  2. lemma OAI.PiExponentSeshadri.Geometry.moduleTensorIso_inv line 19
  3. def OAI.PiExponentSeshadri.Geometry.tensorInclusion line 22
  4. lemma OAI.PiExponentSeshadri.Geometry.frame_square line 26
  5. lemma OAI.PiExponentSeshadri.Geometry.frame_inclusion line 39
  6. lemma OAI.PiExponentSeshadri.Geometry.mono_iso_sandwich line 46
  7. lemma OAI.PiExponentSeshadri.Geometry.tensor_inclusion_framed line 50
  8. theorem OAI.PiExponentSeshadri.Geometry.tensorInclusion_mono line 94
  9. lemma OAI.PiExponentSeshadri.Geometry.tensor_inclusion_ideal line 113