OAI/RingTheory/Multiplicity/TensorPushout.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.TensorPushout.aux line 16
2. lemma OAI.Lech.TensorPushout.aux_tmul line 23
3. def OAI.Lech.TensorPushout.equiv line 26
4. lemma OAI.Lech.TensorPushout.equiv_tmul line 44
5. def OAI.Lech.TensorConductor.congrLeft line 53
6. lemma OAI.Lech.TensorConductor.congrLeft_tmul line 57