OAI/RingTheory/Multiplicity/IdealQuotientFunctor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.TensorIdeal.quotientFunctor line 14
  2. instance OAI.Lech.TensorIdeal.quotientFunctor_additive line 30
  3. lemma OAI.Lech.TensorIdeal.quotientFunctor_map_mk line 38
  4. def OAI.Lech.TensorIdeal.quotientNat line 43
  5. def OAI.Lech.TensorIdeal.tensorQuotientIso line 52
  6. def OAI.Lech.TensorIdeal.quotientPiEquiv line 71
  7. lemma OAI.Lech.TensorIdeal.quotientPiEquiv_mk line 80
  8. lemma OAI.Lech.TensorIdeal.mem_smul_pi_iff line 92
  9. lemma OAI.Lech.TensorIdeal.quotient_torsion line 107
  10. lemma OAI.Lech.TensorIdeal.quotientPiMap_square line 124
  11. lemma OAI.Lech.TensorIdeal.quotientPiMap_factor line 133
  12. lemma OAI.Lech.TensorIdeal.quotientPi_isoModSerre line 148