PUnit

📁 Source: Mathlib/Algebra/GCDMonoid/PUnit.lean

Statistics

Metric	Count
Definitions normalizedGCDMonoid	1
Theorems gcd_eq, lcm_eq, norm_unit_eq	3
Total	4

PUnit

Definitions

Name	Category	Theorems
normalizedGCDMonoid 📖	CompOp	3 math math: norm_unit_eq, lcm_eq, gcd_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gcd_eq 📖	mathematical	—	GCDMonoid.gcd CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring commRing NormalizedGCDMonoid.toGCDMonoid normalizedGCDMonoid	—	—
lcm_eq 📖	mathematical	—	GCDMonoid.lcm CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring commRing NormalizedGCDMonoid.toGCDMonoid normalizedGCDMonoid	—	—
norm_unit_eq 📖	mathematical	—	NormalizationMonoid.normUnit CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring commRing NormalizedGCDMonoid.toNormalizationMonoid normalizedGCDMonoid Units MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Units.instOne	—	—

---

← Back to Index