OAI/Algebra/AffineCancellation/ReplicaLift.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ComplexCancellation.SliceDerivative.derivation line 11
2. lemma OAI.ComplexCancellation.SliceDerivative.apply_eq line 16
3. lemma OAI.ComplexCancellation.SliceDerivative.locallyNilpotent line 17
4. instance OAI.ComplexCancellation.Bundle.finiteType line 23
5. lemma OAI.ComplexCancellation.Torsor.extension_base line 36
6. lemma OAI.ComplexCancellation.Torsor.invariant_replica line 40
7. instance OAI.ComplexCancellation.PolynomialTorsor.(instance at line 54) line 54
8. abbrev OAI.ComplexCancellation.PolynomialTorsor.K line 56
9. abbrev OAI.ComplexCancellation.PolynomialTorsor.P line 57
10. def OAI.ComplexCancellation.PolynomialTorsor.ρ line 59
11. lemma OAI.ComplexCancellation.PolynomialTorsor.ρ_injective line 60
12. lemma OAI.ComplexCancellation.PolynomialTorsor.exists_frame line 61
13. def OAI.ComplexCancellation.PolynomialTorsor.toField line 66
14. def OAI.ComplexCancellation.PolynomialTorsor.inverseCoefficient line 69
15. lemma OAI.ComplexCancellation.PolynomialTorsor.inverseCoefficient_comp line 70
16. lemma OAI.ComplexCancellation.PolynomialTorsor.forward_injective line 77