OAI/NumberTheory/PiExponent/Ampleness/WeightedAffineFrame.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PiExponent.WeightedAffineFrame.frame_nonempty_of_isoOpen_eqline 11 - theorem
OAI.PiExponent.WeightedAffineFrame.affineChart_isoOpenline 22 - theorem
OAI.PiExponent.WeightedAffineFrame.affineFrame_nonemptyline 30