Field

📁 Source: Mathlib/Algebra/Order/Positive/Field.lean

Statistics

Metric	Count
Definitions inv, instCommGroupSubtypeLtOfNat, instPowSubtypeLtOfNatInt_mathlib	3
Theorems coe_inv, coe_zpow	2
Total	5

Positive

Definitions

Name	Category	Theorems
instCommGroupSubtypeLtOfNat 📖	CompOp	—
instPowSubtypeLtOfNatInt_mathlib 📖	CompOp	1 math math: coe_zpow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inv 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Subtype.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	—
coe_zpow 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing instPowSubtypeLtOfNatInt_mathlib DivInvMonoid.toZPow DivisionRing.toDivInvMonoid Field.toDivisionRing	—	—

Positive.Subtype

Definitions

Name	Category	Theorems
inv 📖	CompOp	1 math math: Positive.coe_inv

---

← Back to Index