OAI/Topology/ArtinGroups/Realizations/WeightPrincipalProjection.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.weightPrincipalProjectionline 12 - lemma
OAI.HarmonicArtin.weightPrincipalProjection_continuousline 15 - lemma
OAI.HarmonicArtin.weightPrincipalProjection_surjectiveline 20 - theorem
OAI.HarmonicArtin.weightPrincipalProjection_quotientline 25