OAI/Analysis/Kaplansky/Ultrapower/QuasiValue.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KaplanskyConsequences.QuasiValue line 13
2. lemma OAI.KaplanskyConsequences.QuasiValue.spectral_commuting_add line 31
3. def OAI.KaplanskyConsequences.QuasiValue.ofDimensionState line 46
4. def OAI.KaplanskyConsequences.QuasiValue.q line 80
5. lemma OAI.KaplanskyConsequences.QuasiValue.q_nonneg line 82
6. lemma OAI.KaplanskyConsequences.QuasiValue.q_zero line 83
7. lemma OAI.KaplanskyConsequences.QuasiValue.q_star line 84
8. lemma OAI.KaplanskyConsequences.QuasiValue.q_bound line 86
9. lemma OAI.KaplanskyConsequences.QuasiValue.val_scalar_sub line 90
10. lemma OAI.KaplanskyConsequences.QuasiValue.val_shift line 98