OAI/NumberTheory/PiExponent/Approximation/InverseDualRestriction.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PiExponent.InverseFrames.dualMap_restrictline 12 - lemma
OAI.PiExponent.InverseFrames.dualMap_restrict_coefficientline 40 - lemma
OAI.PiExponent.InverseFrames.dualSection_restrict_coefficientline 49