Units

📁 Source: Mathlib/Algebra/Ring/Subring/Units.lean

Statistics

Metric	Count
Definitions posSubgroup	1
Theorems mem_posSubgroup	1
Total	2

Units

Definitions

Name	Category	Theorems
posSubgroup 📖	CompOp	2 math math: index_posSubgroup, mem_posSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_posSubgroup 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Subgroup instGroup SetLike.instMembership Subgroup.instSetLike posSubgroup Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring val	—	—

---

← Back to Index