OAI/MathematicalPhysics/Heisenberg/MatrixUnitLift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Heisenberg.TensorUnits.liftLinear line 11
2. lemma OAI.Heisenberg.TensorUnits.unit_mul_lift line 16
3. lemma OAI.Heisenberg.TensorUnits.lift_mul line 25
4. lemma OAI.Heisenberg.TensorUnits.lift_one line 35
5. def OAI.Heisenberg.TensorUnits.liftAlg line 40
6. lemma OAI.Heisenberg.TensorUnits.liftAlg_apply line 45