OAI/Analysis/Kaplansky/StableFiniteness/FaithfulRepresentation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KaplanskyConsequences.ActualRepresentationHilbert line 13
2. def OAI.KaplanskyConsequences.actualFaithfulMap line 15
3. lemma OAI.KaplanskyConsequences.actualFaithfulMap_apply line 18
4. lemma OAI.KaplanskyConsequences.actualFaithfulMap_star line 21
5. def OAI.KaplanskyConsequences.actualFaithfulRepresentation line 29
6. lemma OAI.KaplanskyConsequences.actualFaithfulRepresentation_injective line 38