OAI/Topology/ArtinGroups/Harmonic/SphericalPositiveCommonMultiple.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.HarmonicArtin.spherical_positive_common_multipleline 13 - theorem
OAI.HarmonicArtin.spherical_positive_lcm_leftline 28