OAI/Analysis/Kaplansky/Ultrapower/DenseUnits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyConsequences.DenseUnits line 13
2. lemma OAI.KaplanskyConsequences.isUnit_positive_shift line 15
3. lemma OAI.KaplanskyConsequences.denseUnits_of_unitary_polar line 19
4. lemma OAI.KaplanskyConsequences.DenseUnits.map line 43
5. lemma OAI.KaplanskyConsequences.DenseUnits.finite line 48