OAI/RingTheory/Multiplicity/HomogeneousFunctor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Lech.Homogeneous.awayAlgebra line 16
  2. def OAI.Lech.Homogeneous.awayAlg line 25
  3. lemma OAI.Lech.Homogeneous.awayAlg_surjective line 33
  4. lemma OAI.Lech.Homogeneous.awayAlg_piece line 37
  5. lemma OAI.Lech.Homogeneous.awayMap_one line 39
  6. lemma OAI.Lech.Homogeneous.awayMap_mul line 41
  7. lemma OAI.Lech.Homogeneous.awayMap_mk line 44
  8. def OAI.Lech.Homogeneous.awayCongr line 51
  9. lemma OAI.Lech.Homogeneous.awayCongr_mk line 54
  10. lemma OAI.Lech.Homogeneous.awayCongr_symm_mk line 60
  11. lemma OAI.Lech.linearEquiv_mem_ideal_smul_top_iff line 68