OAI/Analysis/Kaplansky/Ultrapower/Wandering.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_partial_final line 14
2. lemma OAI.KaplanskyConsequences.QuasiValue.quotQ_partial_add line 18
3. lemma OAI.KaplanskyConsequences.QuasiValue.unitary_of_residual_corner_zero line 32