FunctionField

📁 Source: Mathlib/NumberTheory/ClassNumber/FunctionField.lean

Statistics

Metric	Count
Definitions instFintypeClassGroupSubtypeMemSubalgebraPolynomialRingOfIntegers, classNumber	2
Theorems classNumber_eq_one_iff	1
Total	3

FunctionField

Definitions

Name	Category	Theorems
classNumber 📖	CompOp	1 math math: classNumber_eq_one_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
classNumber_eq_one_iff 📖	mathematical	—	classNumber IsPrincipalIdealRing Subalgebra Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike ringOfIntegers Subalgebra.toSemiring	—	instIsDomain IsScalarTower.right card_classGroup_eq_one_iff ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomial ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc

FunctionField.RingOfIntegers

Definitions

Name	Category	Theorems
instFintypeClassGroupSubtypeMemSubalgebraPolynomialRingOfIntegers 📖	CompOp	—

---

← Back to Index