OAI/NumberTheory/PiExponent/Approximation/TensorMixedSection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.TensorPure.assoc_pure line 16
2. lemma OAI.PiExponentSeshadri.TensorPure.assoc_inv_pure line 64
3. lemma OAI.PiExponentSeshadri.TensorPure.unit_inv_apply line 85
4. lemma OAI.PiExponentSeshadri.TensorPure.power_succ_apply line 96
5. lemma OAI.PiExponentSeshadri.TensorPure.openSection_tensor line 106
6. instance OAI.PiExponentSeshadri.TensorPure.tensorSection_isIso line 118
7. lemma OAI.PiExponentSeshadri.TensorPure.mixed_value_restrict line 123
8. lemma OAI.PiExponentSeshadri.TensorPure.mixed_value_open line 131