OAI/RingTheory/Multiplicity/CarrierOperators.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Lech.CarrierOperators.Carrier line 12
  2. def OAI.Lech.CarrierOperators.Agree line 18
  3. structure OAI.Lech.CarrierOperators.Op line 21
  4. def OAI.Lech.CarrierOperators.Op.id line 30
  5. def OAI.Lech.CarrierOperators.Op.comp line 35
  6. def OAI.Lech.CarrierOperators.Op.add line 40
  7. def OAI.Lech.CarrierOperators.Op.sub line 51
  8. abbrev OAI.Lech.CarrierOperators.Sections line 63
  9. def OAI.Lech.CarrierOperators.toFixed line 65
  10. lemma OAI.Lech.CarrierOperators.toFixed_self line 74
  11. lemma OAI.Lech.CarrierOperators.toFixed_restrict line 80
  12. def OAI.Lech.CarrierOperators.lift line 89
  13. lemma OAI.Lech.CarrierOperators.toFixed_lift line 93
  14. lemma OAI.Lech.CarrierOperators.lift_comp line 103
  15. lemma OAI.Lech.CarrierOperators.lift_id line 111
  16. lemma OAI.Lech.CarrierOperators.lift_add line 117
  17. lemma OAI.Lech.CarrierOperators.lift_sub line 118
  18. lemma OAI.Lech.CarrierOperators.lift_congr line 120