Basic

📁 Source: Mathlib/NumberTheory/NumberField/Units/Basic.lean

Statistics

Metric	Count
Definitions `complexEmbedding`, `instCoeHTCUnitsRingOfIntegers`, `instFintypeSubtypeUnitsRingOfIntegersMemSubgroupTorsion`, `torsion`, `torsionOrder`	5
Theorems `coe_coe`, `coe_injective`, `coe_mul`, `coe_ne_zero`, `coe_neg_one`, `coe_one`, `coe_pow`, `coe_zpow`, `complexEmbedding_apply`, `complexEmbedding_inj`, `complexEmbedding_injective`, `even_torsionOrder`, `instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion`, `instNeZeroNatTorsionOrder`, `instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion`, `map_complexEmbedding_torsion`, `mem_torsion`, `norm`, `pos_at_place`, `rootsOfUnity_eq_one`, `rootsOfUnity_eq_torsion`, `sum_mult_mul_log`, `torsionOrder_eq_two_of_odd_finrank`, `torsionOrder_ne_zero`, `torsionOrder_pos`, `torsion_eq_one_or_neg_one_of_odd_finrank`, `isUnit_iff_norm`, `isUnit_iff`	28
Total	33

NumberField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_iff_norm` 📖	mathematical	—	`IsUnit` `RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingOfIntegers.instCommRing` `abs` `Rat.instLattice` `Rat.addGroup` `RingOfIntegers.val` `Rat.instField` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike` `RingOfIntegers.norm` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `to_charZero`	—	`to_charZero` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `abs_eq_abs` `Rat.RingOfIntegers.isUnit_iff` `RingOfIntegers.isUnit_norm` `to_finiteDimensional` `Rat.instCharZero`

NumberField.Units

Definitions

Name	Category	Theorems
`complexEmbedding` 📖	CompOp	4 math math: `map_complexEmbedding_torsion`, `complexEmbedding_injective`, `complexEmbedding_apply`, `complexEmbedding_inj`
`instCoeHTCUnitsRingOfIntegers` 📖	CompOp	—
`instFintypeSubtypeUnitsRingOfIntegersMemSubgroupTorsion` 📖	CompOp	—
`torsion` 📖	CompOp	39 math math: `instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion`, `NumberField.IsCMField.unitsComplexConj_torsion`, `NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst`, `NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply`, `NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst`, `map_complexEmbedding_torsion`, `logEmbeddingQuot_apply`, `NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe`, `fundSystem_mk`, `NumberField.IsCMField.indexRealUnits_mul_eq`, `dirichletUnitTheorem.map_logEmbedding_sup_torsion`, `NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion`, `NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer`, `rank_modTorsion`, `NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion`, `NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply`, `mem_torsion`, `regOfFamily_div_regulator`, `NumberField.IsCMField.closure_realFundSystem_sup_torsion`, `instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion`, `closure_fundSystem_sup_torsion_eq_top`, `torsion_eq_one_or_neg_one_of_odd_finrank`, `dirichletUnitTheorem.logEmbedding_eq_zero_iff`, `NumberField.IsCMField.unitsMulComplexConjInv_ker`, `NumberField.IsCMField.unitsMulComplexConjInv_apply`, `NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff`, `rootsOfUnity_eq_torsion`, `logEmbeddingQuot_injective`, `Ideal.torsionMapQuot_injective`, `NumberField.IsCMField.indexRealUnits_eq_two_iff`, `logEmbeddingEquiv_apply`, `exist_unique_eq_mul_prod`, `finiteIndex_iff_sup_torsion_finiteIndex`, `instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion`, `dirichletUnitTheorem.logEmbedding_ker`, `NumberField.IsCMField.map_unitsMulComplexConjInv_torsion`, `NumberField.IsCMField.complexConj_torsion`, `NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd`, `instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion`
`torsionOrder` 📖	CompOp	14 math math: `IsCyclotomicExtension.Rat.torsionOrder_eq`, `NumberField.dedekindZeta_residue_def`, `torsionOrder_pos`, `NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le`, `NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion`, `map_complexEmbedding_torsion`, `instNeZeroNatTorsionOrder`, `torsionOrder_eq_two_of_odd_finrank`, `NumberField.Ideal.tendsto_norm_le_div_atTop₀`, `rootsOfUnity_eq_torsion`, `NumberField.Ideal.tendsto_norm_le_div_atTop`, `NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop`, `dvd_torsionOrder_of_isPrimitiveRoot`, `even_torsionOrder`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_coe` 📖	mathematical	—	`NumberField.RingOfIntegers.val` `Units.val` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring`	—	—
`coe_injective` 📖	mathematical	—	`Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val`	—	`NumberField.RingOfIntegers.coe_injective` `Units.val_injective`
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `RingHom` `NumberField.RingOfIntegers` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—
`coe_ne_zero` 📖	—	—	—	—	`Subtype.coe_injective` `Units.ne_zero` `NumberField.RingOfIntegers.instNontrivial`
`coe_neg_one` 📖	mathematical	—	`DFunLike.coe` `RingHom` `NumberField.RingOfIntegers` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Units.instOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `RingHom` `NumberField.RingOfIntegers` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `RingHom` `NumberField.RingOfIntegers` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Monoid.toNatPow` `Units.instMonoid`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Units.val_pow_eq_pow_val`
`coe_zpow` 📖	mathematical	—	`DFunLike.coe` `RingHom` `NumberField.RingOfIntegers` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `DivInvMonoid.toZPow` `Units.instDivInvMonoid` `DivisionRing.toDivInvMonoid`	—	`map_zpow` `MonoidHom.instMonoidHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`complexEmbedding_apply` 📖	mathematical	—	`Units.val` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `DFunLike.coe` `MonoidHom` `Units` `NumberField.RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `complexEmbedding` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring`	—	—
`complexEmbedding_inj` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Complex` `Complex.instSemiring` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `complexEmbedding`	—	`complexEmbedding_injective`
`complexEmbedding_injective` 📖	mathematical	—	`Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Complex` `Complex.instSemiring` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `complexEmbedding`	—	`Units.map_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `Complex.instNontrivial` `NumberField.RingOfIntegers.coe_injective`
`even_torsionOrder` 📖	mathematical	—	`Even` `torsionOrder`	—	`neg_one_mem_torsion` `Subgroup.orderOf_coe` `orderOf_units` `Units.val_neg` `Units.val_one` `orderOf_neg_one` `NumberField.RingOfIntegers.instNontrivial` `ringChar.eq_zero` `NumberField.RingOfIntegers.instCharZero_1` `NumberField.to_charZero` `Nat.instAtLeastTwoHAddOfNat` `even_iff_two_dvd` `orderOf_dvd_card`
`instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion` 📖	mathematical	—	`IsCyclic` `Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `torsion` `Subgroup.zpow`	—	`subgroup_units_cyclic` `NumberField.RingOfIntegers.instIsDomain` `Finite.of_fintype`
`instNeZeroNatTorsionOrder` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `torsionOrder`	—	`Fintype.instNeZeroNatCardOfNonempty` `instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion`
`instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion` 📖	mathematical	—	`Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `torsion`	—	`One.instNonempty`
`map_complexEmbedding_torsion` 📖	mathematical	—	`Subgroup.map` `Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Units.instGroup` `Complex` `Complex.instSemiring` `complexEmbedding` `torsion` `rootsOfUnity` `torsionOrder` `CommRing.toCommMonoid` `Complex.commRing`	—	`Subgroup.eq_of_le_of_card_ge` `Finite.of_fintype` `instNeZeroNatTorsionOrder` `instIsDomain` `rootsOfUnity_eq_torsion` `map_rootsOfUnity` `complexEmbedding_injective` `Nat.card_eq_fintype_card` `Complex.card_rootsOfUnity` `Nat.card_congr` `torsionOrder.eq_1` `le_refl`
`mem_torsion` 📖	mathematical	—	`Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `torsion` `DFunLike.coe` `NumberField.InfinitePlace` `Real` `NumberField.InfinitePlace.instFunLikeReal` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `Real.instOne`	—	`NumberField.InfinitePlace.eq_iff_eq` `torsion.eq_1` `CommGroup.mem_torsion` `IsOfFinOrder.norm_eq_one` `NormedDivisionRing.toNormMulClass` `NormedDivisionRing.to_normOneClass` `MonoidHom.isOfFinOrder` `isOfFinOrder_iff_pow_eq_one` `NumberField.Embeddings.pow_eq_one_of_norm_eq_one` `Complex.isAlgClosed` `Complex.instCharZero` `NumberField.RingOfIntegers.isIntegral_coe` `Units.ext` `NumberField.RingOfIntegers.ext` `NumberField.RingOfIntegers.coe_eq_algebraMap` `coe_pow` `coe_one`
`norm` 📖	mathematical	—	`abs` `Rat.instLattice` `Rat.addGroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Rat.commRing` `MonoidHom.instFunLike` `Algebra.norm` `DivisionRing.toRatAlgebra` `NumberField.to_charZero` `RingHom` `NumberField.RingOfIntegers` `NumberField.RingOfIntegers.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`NumberField.to_charZero` `RingOfIntegers.coe_norm` `NumberField.isUnit_iff_norm` `Units.isUnit`
`pos_at_place` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `NumberField.InfinitePlace` `NumberField.InfinitePlace.instFunLikeReal` `RingHom` `NumberField.RingOfIntegers` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`NumberField.InfinitePlace.pos_iff` `coe_ne_zero`
`rootsOfUnity_eq_one` 📖	mathematical	`PNat.val` `torsionOrder`	`Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subgroup` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `rootsOfUnity` `Units.instOne`	—	`mem_rootsOfUnity` `orderOf_eq_one_iff` `Nat.eq_one_of_dvd_coprimes` `orderOf_dvd_of_pow_eq_one` `torsion.eq_1` `CommGroup.mem_torsion` `isOfFinOrder_iff_pow_eq_one` `Subtype.prop` `orderOf_submonoid` `orderOf_dvd_card` `one_pow`
`rootsOfUnity_eq_torsion` 📖	mathematical	—	`rootsOfUnity` `torsionOrder` `NumberField.RingOfIntegers` `CommRing.toCommMonoid` `NumberField.RingOfIntegers.instCommRing` `torsion`	—	`Subgroup.ext` `torsion.eq_1` `mem_rootsOfUnity` `CommGroup.mem_torsion` `isOfFinOrder_iff_pow_eq_one` `torsionOrder_pos` `pow_card_eq_one`
`sum_mult_mul_log` 📖	mathematical	—	`Finset.sum` `NumberField.InfinitePlace` `Real` `Real.instAddCommMonoid` `Finset.univ` `NumberField.InfinitePlace.NumberField.InfinitePlace.fintype` `Real.instMul` `Real.instNatCast` `NumberField.InfinitePlace.mult` `Real.log` `DFunLike.coe` `NumberField.InfinitePlace.instFunLikeReal` `RingHom` `NumberField.RingOfIntegers` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `NumberField.RingOfIntegers.instAlgebra_1` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `Semifield.toCommSemiring` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Real.instZero`	—	`NumberField.to_charZero` `Real.log_prod` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instNontrivial` `NumberField.InfinitePlace.instMonoidWithZeroHomClassReal` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `NumberField.RingOfIntegers.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `NumberField.RingOfIntegers.instIsTorsionFree_2` `NumberField.RingOfIntegers.instNontrivial` `Finset.sum_congr` `Real.log_pow` `norm` `Rat.cast_one` `Real.log_one` `NumberField.InfinitePlace.prod_eq_abs_norm`
`torsionOrder_eq_two_of_odd_finrank` 📖	mathematical	`Odd` `Nat.instSemiring` `Module.finrank` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Rat.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `NumberField.to_charZero`	`torsionOrder`	—	`NumberField.to_charZero` `Finset.card_eq_two` `neg_one_mem_torsion` `NumberField.RingOfIntegers.instCharZero_1` `Finset.ext` `Finset.mem_insert` `Finset.mem_singleton` `torsion_eq_one_or_neg_one_of_odd_finrank` `Finset.mem_univ`
`torsionOrder_ne_zero` 📖	—	—	—	—	`instNeZeroNatTorsionOrder`
`torsionOrder_pos` 📖	mathematical	—	`torsionOrder`	—	`instNeZeroNatTorsionOrder`
`torsion_eq_one_or_neg_one_of_odd_finrank` 📖	mathematical	`Odd` `Nat.instSemiring` `Module.finrank` `Rat.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Rat.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `NumberField.to_charZero`	`Units` `NumberField.RingOfIntegers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `torsion` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg`	—	`NumberField.to_charZero` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `sub_eq_zero_of_eq` `Nat.cast_zero` `NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt` `orderOf_submonoid` `orderOf_units` `IsPrimitiveRoot.orderOf` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `CharP.orderOf_eq_two_iff` `NumberField.RingOfIntegers.instNontrivial` `IsDomain.to_noZeroDivisors` `NumberField.RingOfIntegers.instIsDomain` `CharP.ofCharZero` `NumberField.RingOfIntegers.instCharZero_1` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_le_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `orderOf_eq_one_iff` `orderOf_pos_iff` `CommGroup.mem_torsion`

Rat.RingOfIntegers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_iff` 📖	mathematical	—	`IsUnit` `NumberField.RingOfIntegers` `Rat.instField` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `NumberField.RingOfIntegers.val`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `isUnit_map_iff` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `isLocalHom_toRingHom` `isLocalHom_equiv` `RingEquivClass.toMulEquivClass` `Subtype.coe_injective`

---

← Back to Index