Documentation Verification Report

Different

📁 Source: Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

Statistics

Metric	Count
Definitions	0
Theorems `absNorm_differentIdeal`, `discr_dvd_discr`, `discr_mem_differentIdeal`, `isCoprime_differentIdeal_of_isCoprime_discr`, `linearDisjoint_of_isGalois_isCoprime_discr`, `natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow`, `natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow`	7
Total	7

NumberField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absNorm_differentIdeal` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `instNontrivialOfCharZero` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Module.free_of_finite_type_torsion_free'` `Int.instCommRing` `Ring.toAddCommGroup` `AddCommGroup.toIntModule` `EuclideanDomain.to_principal_ideal_domain` `Int.euclideanDomain` `Int.instIsDomain` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `IsDomain.toIsCancelMulZero` `IsDedekindDomain.toIsDomain` `differentIdeal` `Ring.toIntAlgebra` `discr`	—	`Int.instIsDomain` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `IsDomain.toIsCancelMulZero` `IsDedekindDomain.toIsDomain` `AddSubgroup.relIndex_top_right` `RingHomSurjective.ids` `Submodule.comap_map_eq_of_injective` `FaithfulSMul.algebraMap_injective` `IsFractionRing.instFaithfulSMul` `AddSubgroup.relIndex_comap` `RingHomInvPair.ids` `mul_one` `inv_mul_cancel₀` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toNontrivial` `Algebra.IsSeparable.isAlgebraic` `FractionRing.instNontrivial` `Int.instNontrivial` `Algebra.IsSeparable.of_integral` `instIsDomain` `Algebra.IsIntegral.of_finite` `instFiniteDimensionalFractionRingOfFinite` `IsFractionRing.charZero` `Int.instCharZero` `PerfectField.ofCharZero` `FractionalIdeal.coeIdeal_le_one` `le_inv_of_le_inv₀` `PosMulReflectLE.toPosMulReflectLT` `FractionalIdeal.instPosMulReflectLENonZeroDivisors` `MulPosReflectLE.toMulPosReflectLT` `FractionalIdeal.instMulPosReflectLENonZeroDivisors` `FractionalIdeal.instCanonicallyOrderedAdd` `inv_one` `one_ne_zero` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors` `Nat.card_congr` `FractionalIdeal.coe_one` `to_charZero` `AddCommGroup.intIsScalarTower` `Rat.isFractionRing` `to_finiteDimensional` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `Rat.instCharZero` `IsDomain.to_noZeroDivisors` `coeIdeal_differentIdeal` `inv_inv` `RingOfIntegers.instFreeInt` `Finite.of_fintype` `Module.IsNoetherian.finite` `RingOfIntegers.instIsNoetherianInt` `traceForm_nondegenerate` `Submodule.ext` `RingOfIntegers.instIsIntegralClosureInt` `Equiv.exists_congr_left` `IsIntegralClosure.algebraMap_equiv` `mem_span_integralBasis` `Int.natCast_natAbs` `Int.cast_natCast` `Int.cast_abs` `Rat.instIsStrictOrderedRing` `instNontrivialOfCharZero` `AddSubgroup.relIndex_eq_abs_det` `Submodule.toAddSubgroup_le` `FractionalIdeal.one_le_dual_one` `OrderIso.injective` `AddSubgroup.toIntSubmodule_closure` `Submodule.toIntSubmodule_toAddSubgroup` `LinearMap.BilinForm.dualSubmodule_span_of_basis` `FractionalIdeal.coe_dual_one` `eq_intCast` `RingHom.instRingHomClass` `RingHom.map_det` `Matrix.ext` `integralBasis_apply` `LinearMap.BilinForm.dualBasis_repr_apply` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Algebra.trace_localization` `RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `mul_comm`
`discr_dvd_discr` 📖	mathematical	—	`discr`	—	`instNontrivialOfCharZero` `RingOfIntegers.instCharZero_1` `to_charZero` `RingOfIntegers.instIsDedekindDomain` `RingOfIntegers.instFreeInt` `IsDedekindDomain.toIsDomain` `RingOfIntegers.instIsTorsionFree_1` `natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsIntegralClosureInt` `Module.IsNoetherian.finite` `RingOfIntegers.instIsNoetherianInt` `RingOfIntegers.instIsScalarTower` `RingOfIntegers.instIsScalarTower_1` `RingOfIntegers.extension_isNoetherian` `Nat.cast_mul` `Nat.cast_pow` `mul_pow` `mul_assoc` `mul_comm` `dvd_trans` `dvd_pow_self` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instFiniteDimensional` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`discr_mem_differentIdeal` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `differentIdeal` `Int.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing` `Int.instIsDomain` `instIsTorsionFreeIntOfIsAddTorsionFree` `Ring.toAddCommGroup` `IsAddTorsionFree.of_isCancelMulZero_charZero` `IsDomain.toIsCancelMulZero` `IsDedekindDomain.toIsDomain` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `discr`	—	`Int.instIsDomain` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `IsDomain.toIsCancelMulZero` `IsDedekindDomain.toIsDomain` `instNontrivialOfCharZero` `Module.free_of_finite_type_torsion_free'` `EuclideanDomain.to_principal_ideal_domain` `Ideal.absNorm_mem` `Int.cast_natCast` `absNorm_differentIdeal` `neg_mem_iff` `NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClassIdeal` `Int.cast_neg`
`isCoprime_differentIdeal_of_isCoprime_discr` 📖	mathematical	`IsCoprime` `Int.instCommSemiring` `discr`	`Ideal` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingOfIntegers.instCommRing` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `inst_ringOfIntegersAlgebra` `differentIdeal` `Int.instCommRing` `Ring.toIntAlgebra` `CommRing.toRing` `Int.instIsDomain` `RingOfIntegers.instIsDedekindDomain` `instIsTorsionFreeIntOfIsAddTorsionFree` `Ring.toAddCommGroup` `IsAddTorsionFree.of_isCancelMulZero_charZero` `RingOfIntegers.instCharZero_1` `to_charZero` `IsDomain.toIsCancelMulZero` `RingOfIntegers.instIsDomain`	—	`Int.instIsDomain` `RingOfIntegers.instIsDedekindDomain` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `RingOfIntegers.instCharZero_1` `to_charZero` `IsDomain.toIsCancelMulZero` `RingOfIntegers.instIsDomain` `Ideal.isCoprime_iff_exists` `Ideal.mul_mem_left` `map_intCast` `RingHom.instRingHomClass` `Ideal.mem_map_of_mem` `discr_mem_differentIdeal` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsIntegralClosureInt` `Module.IsNoetherian.finite` `RingOfIntegers.instIsNoetherianInt` `Int.cast_mul` `Int.cast_add` `Int.cast_one`
`linearDisjoint_of_isGalois_isCoprime_discr` 📖	mathematical	`IsCoprime` `Int.instCommSemiring` `discr` `IntermediateField` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `to_charZero` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `of_intermediateField` `Rat.numberField`	`IntermediateField.LinearDisjoint` `Function.Injective.divisionRing` `Subfield` `Subfield.instSetLike` `IntermediateField.toSubfield` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `SubringClass.toCommRing` `NegMemClass.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `AddSubgroupClass.sub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `OneMemClass.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toMul` `InvMemClass.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `SubgroupClass.div` `DivisionRing.toDivInvMonoid` `AddSubmonoidClass.nSMul` `AddMonoidWithOne.toAddMonoid` `AddSubgroupClass.zsmul` `SubfieldClass.instSMulNNRat` `SubfieldClass.instSMulRat` `SubmonoidClass.nPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SubgroupClass.zpow` `AddMonoidWithOne.toNatCast` `SubfieldClass.toDivisionRing` `AddGroupWithOne.toIntCast` `SubfieldClass.instNNRatCast` `SubfieldClass.instRatCast` `IntermediateField.charZero` `Rat.instCharZero` `IntermediateField.instAlgebraSubtypeMem` `Algebra.id` `Semifield.toCommSemiring` `IsScalarTower.rat` `CommRing.toRing` `IntermediateField.instModuleSubtypeMem` `AddCommGroup.toAddCommMonoid` `Semiring.toModule` `IntermediateField.module'` `Rat.semiring` `Algebra.toSMul` `Rat.commSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace`	—	`to_charZero` `IntermediateField.charZero` `Rat.instCharZero` `of_intermediateField` `Rat.numberField` `IntermediateField.LinearDisjoint.of_inf_eq_bot` `to_finiteDimensional` `IsCoprime.isUnit_of_dvd'` `discr_dvd_discr` `Mathlib.Tactic.Contrapose.contrapose₁` `IsScalarTower.rat` `LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `Rat.nontrivial` `Rat.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsScalarTower.left` `IntermediateField.finrank_eq_one_iff` `Iff.not` `Int.isUnit_iff_abs_eq` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Int.instCharZero` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `abs_discr_gt_two`
`natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow` 📖	mathematical	—	`discr` `DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `instNontrivialOfCharZero` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `differentIdeal` `IsDedekindDomain.toIsDomain` `Monoid.toNatPow` `Nat.instMonoid` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`instNontrivialOfCharZero` `Int.instIsDomain` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `IsDomain.toIsCancelMulZero` `IsDedekindDomain.toIsDomain` `IsScalarTower.right` `differentIdeal_eq_differentIdeal_mul_differentIdeal` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `EuclideanDomain.to_principal_ideal_domain` `AddCommGroup.intIsScalarTower` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toNontrivial` `Algebra.IsSeparable.isAlgebraic` `FractionRing.instNontrivial` `Int.instNontrivial` `Algebra.IsSeparable.of_integral` `instIsDomain` `Algebra.IsIntegral.of_finite` `instFiniteDimensionalFractionRingOfFinite` `IsFractionRing.charZero` `Int.instCharZero` `PerfectField.ofCharZero` `Algebra.finrank_eq_of_equiv_equiv` `RingHom.ext` `IsFractionRing.algEquiv_commutes` `Localization.isLocalization` `FractionRing.instIsScalarTower` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `Module.free_of_finite_type_torsion_free'` `absNorm_differentIdeal` `Ideal.absNorm_algebraMap` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow` 📖	mathematical	`IntermediateField.LinearDisjoint` `Rat.instField` `DivisionRing.toRatAlgebra` `Field.toDivisionRing` `to_charZero` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `Function.Injective.divisionRing` `Subfield` `Subfield.instSetLike` `IntermediateField.toSubfield` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `SubringClass.toCommRing` `NegMemClass.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `AddSubgroupClass.sub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `OneMemClass.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toMul` `InvMemClass.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `SubgroupClass.div` `DivisionRing.toDivInvMonoid` `AddSubmonoidClass.nSMul` `AddMonoidWithOne.toAddMonoid` `AddSubgroupClass.zsmul` `SubfieldClass.instSMulNNRat` `SubfieldClass.instSMulRat` `SubmonoidClass.nPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SubgroupClass.zpow` `AddMonoidWithOne.toNatCast` `SubfieldClass.toDivisionRing` `AddGroupWithOne.toIntCast` `SubfieldClass.instNNRatCast` `SubfieldClass.instRatCast` `IntermediateField.charZero` `Rat.instCharZero` `IntermediateField.instAlgebraSubtypeMem` `Algebra.id` `Semifield.toCommSemiring` `IsScalarTower.rat` `CommRing.toRing` `IntermediateField.instModuleSubtypeMem` `AddCommGroup.toAddCommMonoid` `Semiring.toModule` `IntermediateField.module'` `Rat.semiring` `Algebra.toSMul` `Rat.commSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Rat.instNormedField` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsCoprime` `Ideal` `RingOfIntegers` `CommRing.toCommSemiring` `RingOfIntegers.instCommRing` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `inst_ringOfIntegersAlgebra` `differentIdeal` `Int.instCommRing` `Ring.toIntAlgebra` `Int.instIsDomain` `RingOfIntegers.instIsDedekindDomain` `of_intermediateField` `Rat.numberField` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `RingOfIntegers.instCharZero_1` `IsDomain.toIsCancelMulZero` `RingOfIntegers.instIsDomain`	`discr` `Monoid.toNatPow` `Nat.instMonoid` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`to_charZero` `IntermediateField.charZero` `Rat.instCharZero` `IsScalarTower.rat` `Int.instIsDomain` `RingOfIntegers.instIsDedekindDomain` `of_intermediateField` `Rat.numberField` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `RingOfIntegers.instCharZero_1` `IsDomain.toIsCancelMulZero` `RingOfIntegers.instIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `RingOfIntegers.instNontrivial` `RingOfIntegers.instIsTorsionFree_1` `instNontrivialOfCharZero` `RingOfIntegers.instFreeInt` `IsDedekindDomain.toIsDomain` `natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsIntegralClosureInt` `Module.IsNoetherian.finite` `RingOfIntegers.instIsNoetherianInt` `RingOfIntegers.instIsScalarTower` `RingOfIntegers.instIsScalarTower_1` `RingOfIntegers.extension_isNoetherian` `IsScalarTower.left` `IntermediateField.LinearDisjoint.finrank_left_eq_finrank` `to_finiteDimensional` `IsDomain.toNontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Algebra.finrank_eq_of_equiv_equiv` `RingHom.ext` `IsFractionRing.algEquiv_commutes` `Localization.isLocalization` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `RingOfIntegers.inst_isScalarTower` `IntermediateField.LinearDisjoint.finrank_right_eq_finrank` `Module.free_of_finite_type_torsion_free'` `EuclideanDomain.to_principal_ideal_domain` `absNorm_differentIdeal` `Ideal.absNorm_algebraMap` `RingOfIntegers.instIsIntegrallyClosed` `IsDedekindDomain.differentIdeal_eq_map_differentIdeal` `Rat.isFractionRing` `AddCommGroup.intIsScalarTower` `RingOfIntegers.instIsTorsionFree_2` `IntermediateField.isSeparable_tower_bot` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `Rat.nontrivial` `PerfectField.ofCharZero` `IntermediateField.isSeparable_tower_top` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `RingOfIntegers.instIsIntegralClosure` `Algebra.IsSeparable.isAlgebraic` `FractionRing.instNontrivial` `Int.instNontrivial` `Algebra.IsSeparable.of_integral` `instIsDomain` `Algebra.IsIntegral.of_finite` `instFiniteDimensionalFractionRingOfFinite` `IsFractionRing.charZero` `Int.instCharZero` `IntermediateField.isScalarTower_mid'` `IntermediateField.linearDisjoint_comm` `sup_comm` `isCoprime_comm`

---

← Back to Index