Documentation Verification Report

FractionalIdeal

📁 Source: Mathlib/NumberTheory/NumberField/FractionalIdeal.lean

Statistics

Metric	Count
Definitions `FractionalIdeal`, `basisOfFractionalIdeal`, `fractionalIdealBasis`	3
Theorems `basisOfFractionalIdeal_apply`, `det_basisOfFractionalIdeal_eq_absNorm`, `fractionalIdeal_rank`, `instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule`, `instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule`, `instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype`, `mem_span_basisOfFractionalIdeal`	7
Total	10

NumberField

Definitions

Name	Category	Theorems
`basisOfFractionalIdeal` 📖	CompOp	5 math math: `det_basisOfFractionalIdeal_eq_absNorm`, `mixedEmbedding.det_basisOfFractionalIdeal_eq_norm`, `mem_span_basisOfFractionalIdeal`, `mixedEmbedding.fractionalIdealLatticeBasis_apply`, `basisOfFractionalIdeal_apply`
`fractionalIdealBasis` 📖	CompOp	1 math math: `basisOfFractionalIdeal_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basisOfFractionalIdeal_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `Module.Free.ChooseBasisIndex` `Submodule` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingRingOfIntegers` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `RingOfIntegers.instAlgebra_1` `SetLike.instMembership` `Submodule.setLike` `FractionalIdeal.coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Units.val` `FractionalIdeal` `MonoidWithZero.toMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `Int.instSemiring` `Submodule.addCommMonoid` `AddCommGroup.toIntModule` `Submodule.addCommGroup` `CommRing.toRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` `Rat.semiring` `Rat.commSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `to_charZero` `Module.Basis.instFunLike` `basisOfFractionalIdeal` `fractionalIdealBasis`	—	`RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` `Module.Basis.ofIsLocalizedModule_apply` `Rat.isFractionRing` `to_charZero` `instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype`
`det_basisOfFractionalIdeal_eq_absNorm` 📖	mathematical	—	`abs` `Rat.instLattice` `Rat.addGroup` `DFunLike.coe` `AlternatingMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Rat.commRing` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.toModule` `Rat.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `to_charZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Module.Free.ChooseBasisIndex` `RingOfIntegers` `Int.instSemiring` `instCommRingRingOfIntegers` `AddCommGroup.toIntModule` `CommRing.toRing` `RingOfIntegers.instFreeInt` `AlternatingMap.instFunLike` `Module.Basis.det` `Module.Free.instDecidableEqChooseBasisIndex` `Module.Free.ChooseBasisIndex.fintype` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `RingOfIntegers.instFG` `integralBasis` `Module.Basis` `Rat.semiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.Basis.instFunLike` `Module.Basis.reindex` `Submodule` `RingOfIntegers.instAlgebra_1` `SetLike.instMembership` `Submodule.setLike` `FractionalIdeal.coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Units.val` `FractionalIdeal` `MonoidWithZero.toMonoid` `FractionalIdeal.semifield` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `Submodule.addCommMonoid` `Submodule.addCommGroup` `instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` `basisOfFractionalIdeal` `Equiv.symm` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `FractionalIdeal.commSemiring` `MonoidWithZeroHom.funLike` `FractionalIdeal.absNorm`	—	`RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `RingOfIntegers.instFreeInt` `instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` `to_charZero` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `RingOfIntegers.instFG` `Rat.isFractionRing` `AddCommGroup.intIsScalarTower` `RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `FractionalIdeal.abs_det_basis_change` `instIsDomain` `Module.Basis.coe_reindex` `basisOfFractionalIdeal_apply`
`fractionalIdeal_rank` 📖	mathematical	—	`Module.finrank` `Submodule` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingRingOfIntegers` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `RingOfIntegers.instAlgebra_1` `SetLike.instMembership` `Submodule.setLike` `FractionalIdeal.coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Units.val` `FractionalIdeal` `MonoidWithZero.toMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `Int.instSemiring` `Submodule.addCommMonoid` `AddCommGroup.toIntModule` `Submodule.addCommGroup` `CommRing.toRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` `instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition` `Int.instNontrivial` `to_charZero` `RingOfIntegers.rank` `Module.finrank_eq_card_basis` `Rat.nontrivial`
`instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` 📖	mathematical	—	`Module.Finite` `Submodule` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingRingOfIntegers` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `RingOfIntegers.instAlgebra_1` `SetLike.instMembership` `Submodule.setLike` `FractionalIdeal.coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Int.instSemiring` `Submodule.addCommMonoid` `AddCommGroup.toIntModule` `Submodule.addCommGroup` `CommRing.toRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Module.Finite.of_surjective` `RingHomSurjective.ids` `Module.instFiniteSubtypeMemIdealOfIsNoetherian` `RingOfIntegers.instIsNoetherianInt` `RingHomInvPair.ids` `LinearMap.CompatibleSMul.intModule` `RingOfIntegers.instIsTorsionFree_2` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `nonZeroDivisors.coe_ne_zero` `LinearEquiv.surjective`
`instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` 📖	mathematical	—	`Module.Free` `Submodule` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingRingOfIntegers` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `RingOfIntegers.instAlgebra_1` `SetLike.instMembership` `Submodule.setLike` `FractionalIdeal.coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Int.instSemiring` `Submodule.addCommMonoid` `AddCommGroup.toIntModule` `Submodule.addCommGroup` `CommRing.toRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Module.Free.of_equiv` `RingHomInvPair.ids` `LinearMap.CompatibleSMul.intModule` `RingOfIntegers.instIsTorsionFree_2` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `nonZeroDivisors.coe_ne_zero` `instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree` `EuclideanDomain.to_principal_ideal_domain` `Int.instIsDomain` `Module.instFiniteSubtypeMemIdealOfIsNoetherian` `RingOfIntegers.instIsNoetherianInt` `Ideal.instIsTorsionFreeSubtypeMemSubmodule` `IsScalarTower.right` `instIsTorsionFreeIntOfIsAddTorsionFree` `IsAddTorsionFree.of_isCancelMulZero_charZero` `RingOfIntegers.instCharZero_1` `to_charZero` `IsDomain.toIsCancelMulZero`
`instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype` 📖	mathematical	—	`IsLocalizedModule` `Int.instCommSemiring` `Submodule` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingRingOfIntegers` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `RingOfIntegers.instAlgebra_1` `SetLike.instMembership` `Submodule.setLike` `FractionalIdeal.coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Units.val` `FractionalIdeal` `MonoidWithZero.toMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `Submodule.addCommMonoid` `AddCommGroup.toIntModule` `Submodule.addCommGroup` `CommRing.toRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Int.instSemiring` `LinearMap.restrictScalars` `Submodule.module` `LinearMap.CompatibleSMul.intModule` `Submodule.subtype`	—	`RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `LinearMap.CompatibleSMul.intModule` `smulCommClass_self` `IsScalarTower.left` `AlgHom.commutes` `Algebra.lmul_isUnit_iff` `isUnit_iff_ne_zero` `eq_intCast` `RingHom.instRingHomClass` `Int.cast_ne_zero` `to_charZero` `nonZeroDivisors.coe_ne_zero` `Int.instNontrivial` `IsLocalization.surj` `RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors` `RingOfIntegers.instFreeInt` `FractionalIdeal.num_le` `IsLocalization.mem_coeSubmodule` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `Ideal.absNorm_mem` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_natCast` `Submonoid.mul_mem` `mem_nonZeroDivisors_of_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.cast_ne_zero` `Int.instCharZero` `Ideal.absNorm_eq_zero_iff` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `RingOfIntegers.instFG` `Iff.not` `FractionalIdeal.num_eq_zero_iff` `Units.ne_zero` `FractionalIdeal.instNontrivialNonZeroDivisors` `zsmul_eq_mul` `Int.cast_mul` `Int.cast_natCast` `map_intCast` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `one_smul` `Submodule.injective_subtype`
`mem_span_basisOfFractionalIdeal` 📖	mathematical	—	`Submodule` `Int.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Module.Free.ChooseBasisIndex` `RingOfIntegers` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingRingOfIntegers` `Algebra.toModule` `RingOfIntegers.instAlgebra_1` `FractionalIdeal.coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Units.val` `FractionalIdeal` `MonoidWithZero.toMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FractionalIdeal.semifield` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `Submodule.addCommMonoid` `Submodule.addCommGroup` `CommRing.toRing` `instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` `DFunLike.coe` `Module.Basis` `Rat.semiring` `Rat.commSemiring` `Field.toSemifield` `DivisionRing.toRatAlgebra` `to_charZero` `Module.Basis.instFunLike` `basisOfFractionalIdeal` `Set` `Set.instMembership` `SetLike.coe` `FractionalIdeal.instSetLike`	—	`RingOfIntegers.instIsFractionRing` `RingOfIntegers.instIsDedekindDomain` `instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule` `to_charZero` `Rat.isFractionRing` `instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype` `basisOfFractionalIdeal.eq_1` `RingHomSurjective.ids` `Module.Basis.ofIsLocalizedModule_span`

(root)

Definitions

Name	Category	Theorems
`FractionalIdeal` 📖	CompOp	294 math math: `FractionalIdeal.le_spanSingleton_mul_iff`, `FractionalIdeal.coeIdeal_top`, `FractionalIdeal.canonicalEquiv_trans_canonicalEquiv`, `FractionalIdeal.spanSingleton_inv_mul`, `FractionalIdeal.spanSingleton_mul_inv`, `FractionalIdeal.eq_zero_iff`, `FractionalIdeal.mapEquiv_apply`, `FractionalIdeal.finprod_heightOneSpectrum_factorization_principal`, `Ideal.hasFiniteMulSupport_coe`, `ClassGroup.mk0_integralRep`, `FractionalIdeal.sup_eq_add`, `FractionalIdeal.mul_eq_mul`, `ClassGroup.mk_eq_mk_of_coe_ideal`, `FractionalIdeal.coeIdealHom_apply`, `FractionalIdeal.map_one_div`, `NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd`, `ClassGroup.Quot_mk_eq_mk`, `FractionalIdeal.le_dual_iff`, `FractionalIdeal.fg_unit`, `FractionalIdeal.mem_adjoinIntegral_self`, `FractionalIdeal.sup_mul_inf`, `FractionalIdeal.instNontrivialNonZeroDivisors`, `FractionalIdeal.inv_anti_mono`, `FractionalIdeal.mul_inv_cancel_of_le_one`, `NumberField.mixedEmbedding.mem_idealLattice`, `FractionalIdeal.one_mem_one`, `FractionalIdeal.invertible_of_principal`, `FractionalIdeal.coe_le_coe`, `FractionalIdeal.coe_extendedHomₐ_eq_span`, `mem_principal_ideals_iff`, `FractionalIdeal.absNorm_eq'`, `FractionalIdeal.one_le`, `FractionalIdeal.divMod_zero_left`, `FractionalIdeal.count_finsuppProd`, `FractionalIdeal.coe_mem_one`, `FractionalIdeal.coe_inf`, `FractionalIdeal.coeIdeal_le_one`, `FractionalIdeal.div_one`, `FractionalIdeal.spanFinset_eq_zero`, `FractionalIdeal.inv_le_inv_iff`, `FractionalIdeal.right_inverse_eq`, `FractionalIdeal.instMulPosStrictMonoNonZeroDivisors`, `FractionalIdeal.extendedHomₐ_coeIdeal_eq_map`, `FractionalIdeal.le_div_iff_mul_le`, `FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal`, `FractionalIdeal.inf_mul`, `FractionalIdeal.spanSingleton_mul_spanSingleton`, `FractionalIdeal.isUnit_num`, `FractionalIdeal.eq_zero_or_one_of_isField`, `FractionalIdeal.le_self_mul_inv`, `FractionalIdeal.le_div_iff_of_ne_zero`, `FractionalIdeal.instMulPosReflectLENonZeroDivisors`, `FractionalIdeal.mapEquiv_symm`, `FractionalIdeal.div_of_ne_zero`, `FractionalIdeal.inv_eq`, `FractionalIdeal.le_zero_iff`, `FractionalIdeal.coe_pow`, `FractionalIdeal.mem_map`, `FractionalIdeal.zero_of_num_eq_bot`, `FractionalIdeal.extendedHom_apply`, `FractionalIdeal.spanSingleton_le_iff_mem`, `FractionalIdeal.dual_eq_dual_mul_dual`, `FractionalIdeal.canonicalEquiv_symm`, `FractionalIdeal.count_finprod_coprime`, `FractionalIdeal.coeIdeal_sup`, `FractionalIdeal.one_div_spanSingleton`, `FractionalIdeal.finprod_heightOneSpectrum_factorization`, `FractionalIdeal.one_le_dual_one`, `NumberField.mixedEmbedding.fundamentalDomain_idealLattice`, `coe_toPrincipalIdeal`, `FractionalIdeal.le_one_iff_exists_coeIdeal`, `FractionalIdeal.count_prod`, `FractionalIdeal.coe_nsmul`, `WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul`, `FractionalIdeal.extended_le_one_of_le_one`, `NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis`, `FractionalIdeal.count_finprod`, `FractionalIdeal.coe_natCast`, `FractionalIdeal.count_ne_zero`, `NumberField.det_basisOfFractionalIdeal_eq_absNorm`, `FractionalIdeal.spanSingleton_pow`, `FractionalIdeal.spanSingleton_mul_le_iff`, `FractionalIdeal.absNorm_bot`, `FractionalIdeal.mem_one_iff`, `FractionalIdeal.mem_add`, `FractionalIdeal.mul_left_strictMono`, `FractionalIdeal.coeIdeal_inf`, `FractionalIdeal.extendedHomₐ_injective`, `NumberField.mixedEmbedding.span_idealLatticeBasis`, `differentialIdeal_le_iff`, `FractionalIdeal.coeToSubmodule_eq_bot`, `FractionalIdeal.canonicalEquiv_mk0`, `FractionalIdeal.coe_dual_one`, `FractionalIdeal.extended_zero`, `PrincipalIdeals.normal`, `coeIdeal_differentIdeal`, `FractionalIdeal.eq_one_div_of_mul_eq_one_right`, `FractionalIdeal.one_le_extended_of_one_le`, `FractionalIdeal.inv_le_dual`, `FractionalIdeal.coeIdeal_le_coeIdeal'`, `NumberField.mixedEmbedding.covolume_idealLattice`, `FractionalIdeal.coe_ideal_span_singleton_div_self`, `FractionalIdeal.mul_generator_self_inv`, `FractionalIdeal.le_inv_comm`, `FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul`, `FractionalIdeal.canonicalEquiv_spanSingleton`, `FractionalIdeal.num_zero_eq`, `FractionalIdeal.eq_spanSingleton_mul`, `FractionalIdeal.extendedHomₐ_eq_zero_iff`, `FractionalIdeal.extended_mul`, `FractionalIdeal.coe_add`, `FractionalIdeal.num_le_mul_inv`, `FractionalIdeal.coe_one_eq_coeSubmodule_top`, `FractionalIdeal.extendedHomₐ_eq_one_iff`, `FractionalIdeal.mem_coeIdeal`, `FractionalIdeal.coe_inv_of_ne_zero`, `NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm`, `FractionalIdeal.isNoetherian_zero`, `FractionalIdeal.coeIdeal_injective`, `FractionalIdeal.bot_eq_zero`, `FractionalIdeal.coeIdeal_eq_zero'`, `FractionalIdeal.coe_one`, `FractionalIdeal.coeIdeal_mul`, `FractionalIdeal.map_eq_zero_iff`, `FractionalIdeal.dual_mul_self`, `FractionalIdeal.canonicalEquiv_coeIdeal`, `differentialIdeal_le_fractionalIdeal_iff`, `FractionalIdeal.mem_dual`, `FractionalIdeal.extended_one`, `FractionalIdeal.mem_coeIdeal_of_mem`, `FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top`, `FractionalIdeal.absNorm_eq`, `FractionalIdeal.coe_mul`, `FractionalIdeal.dual_involutive`, `FractionalIdeal.spanSingleton_div_spanSingleton`, `FractionalIdeal.mem_spanSingleton`, `FractionalIdeal.mul_def`, `FractionalIdeal.coeSubmoduleHom_apply`, `FractionalIdeal.mem_zero_iff`, `FractionalIdeal.coeFun_mapEquiv`, `FractionalIdeal.dual_eq_mul_inv`, `FractionalIdeal.dual_div_dual`, `FractionalIdeal.mul_le`, `FractionalIdeal.count_mul`, `FractionalIdeal.dual_zero`, `FractionalIdeal.absNorm_span_singleton`, `FractionalIdeal.mul_one_div_le_one`, `FractionalIdeal.canonicalEquiv_canonicalEquiv`, `FractionalIdeal.count_pow`, `FractionalIdeal.coeIdeal_eq_one`, `NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt`, `one_mem_inv_coe_ideal`, `ClassGroup.mk_mk0`, `NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le`, `FractionalIdeal.isPrincipal_inv`, `FractionalIdeal.coeToSet_coeToSubmodule`, `FractionalIdeal.coe_ideal_mul_inv`, `ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring`, `Ideal.finite_mulSupport_coe`, `FractionalIdeal.map_div`, `FractionalIdeal.spanSingleton_zero`, `ClassGroup.mk_eq_one_iff`, `NumberField.fractionalIdeal_rank`, `FractionalIdeal.map_inv`, `FractionalIdeal.instMulRightMono`, `toPrincipalIdeal_eq_iff`, `FractionalIdeal.ext_iff`, `FractionalIdeal.coeIdeal_bot`, `NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis`, `WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'`, `FractionalIdeal.dual_le_dual`, `FractionalIdeal.mem_span_mul_finite_of_mem_mul`, `FractionalIdeal.exists_ne_zero_mem_isInteger`, `FractionalIdeal.canonicalEquiv_flip`, `ClassGroup.mk_eq_mk`, `FractionalIdeal.count_zpow_self`, `FractionalIdeal.map_mul`, `FractionalIdeal.extended_add`, `FractionalIdeal.smul_mem_dual_one`, `FractionalIdeal.count_neg_zpow`, `FractionalIdeal.zero_mem`, `FractionalIdeal.divMod_zero_right`, `WeierstrassCurve.Affine.Point.toClass_some`, `FractionalIdeal.coe_sup`, `FractionalIdeal.map_one`, `FractionalIdeal.mul_inv_cancel_iff`, `FractionalIdeal.coe_ideal_span_singleton_inv_mul`, `FractionalIdeal.mul_inf`, `NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt'`, `FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal`, `FractionalIdeal.instIsOrderedRing`, `FractionalIdeal.absNorm_nonneg`, `FractionalIdeal.count_zero`, `FractionalIdeal.div_spanSingleton`, `FractionalIdeal.le_one_of_extendedHomₐ_le_one`, `FractionalIdeal.count_one`, `NumberField.mem_span_basisOfFractionalIdeal`, `FractionalIdeal.mem_singleton_mul`, `FractionalIdeal.one_le_extendedHomₐ_iff`, `FractionalIdeal.mem_spanSingleton_self`, `FractionalIdeal.spanSingleton_eq_zero_iff`, `FractionalIdeal.le_self_mul_one_div`, `FractionalIdeal.dual_inv`, `FractionalIdeal.div_zero`, `FractionalIdeal.coeIdeal_eq_zero`, `FractionalIdeal.divMod_spec`, `FractionalIdeal.bot_lt_mul_inv`, `FractionalIdeal.not_inv_le_one_of_ne_bot`, `FractionalIdeal.dual_eq_zero_iff`, `IsDedekindDomain.exists_add_spanSingleton_mul_eq`, `FractionalIdeal.mul_inv_cancel_iff_isUnit`, `FractionalIdeal.instPosMulStrictMonoNonZeroDivisors`, `FractionalIdeal.inv_zero'`, `FractionalIdeal.mem_coe`, `FractionalIdeal.coeToSubmodule_injective`, `FractionalIdeal.eq_zero_or_one`, `NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply`, `FractionalIdeal.exists_eq_spanSingleton_mul`, `FractionalIdeal.count_zpow`, `FractionalIdeal.abs_det_basis_change`, `FractionalIdeal.zero_le`, `FractionalIdeal.count_pow_self`, `FractionalIdeal.map_canonicalEquiv_mk0`, `FractionalIdeal.count_inv`, `FractionalIdeal.mem_canonicalEquiv_apply`, `FractionalIdeal.mapEquiv_refl`, `ClassGroup.mk_eq_one_of_coe_ideal`, `Ideal.finprod_heightOneSpectrum_factorization_coe`, `FractionalIdeal.invertible_iff_generator_nonzero`, `toPrincipalIdeal_def`, `FractionalIdeal.count_mul'`, `FractionalIdeal.dual_inv_le`, `NumberField.basisOfFractionalIdeal_apply`, `FractionalIdeal.spanSingleton_one`, `FractionalIdeal.spanSingleton_div_self`, `Ideal.exist_integer_multiples_notMem`, `FractionalIdeal.equivNum_apply`, `FractionalIdeal.instMulLeftMono`, `FractionalIdeal.coe_ideal_span_singleton_mul_inv`, `ClassGroup.equiv_mk0`, `FractionalIdeal.map_add`, `NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr`, `FractionalIdeal.den_mul_self_eq_num'`, `FractionalIdeal.canonicalEquiv_self`, `FractionalIdeal.inv_le_comm`, `FractionalIdeal.mul_mem_mul`, `FractionalIdeal.dual_injective`, `FractionalIdeal.map_injective`, `FractionalIdeal.self_mul_dual`, `FractionalIdeal.coe_div`, `ClassGroup.mk_canonicalEquiv`, `NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype`, `WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq`, `FractionalIdeal.adjoinIntegral_eq_one_of_isUnit`, `FractionalIdeal.coeIdeal_absNorm`, `FractionalIdeal.coeIdeal_injective'`, `FractionalIdeal.instCanonicallyOrderedAdd`, `Ideal.hasFiniteMulSupport_inv`, `FractionalIdeal.coe_copy`, `FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction`, `FractionalIdeal.absNorm_eq_zero_iff`, `FractionalIdeal.mem_extended_iff`, `FractionalIdeal.trace_mem_dual_one`, `FractionalIdeal.num_eq_zero_iff`, `FractionalIdeal.den_mem_inv`, `Ideal.finite_mulSupport_inv`, `FractionalIdeal.coe_mk0`, `ClassGroup.mk_def`, `FractionalIdeal.num_le`, `WeierstrassCurve.Affine.Point.toClass_apply`, `isDedekindDomainInv_iff`, `FractionalIdeal.zero_divMod`, `FractionalIdeal.mul_right_strictMono`, `FractionalIdeal.mem_div_iff_of_ne_zero`, `FractionalIdeal.coeIdeal_pow`, `FractionalIdeal.le_dual_inv_aux`, `FractionalIdeal.coe_ideal_le_self_mul_inv`, `FractionalIdeal.instPosMulReflectLENonZeroDivisors`, `ClassGroup.equiv_mk`, `FractionalIdeal.extendedHomₐ_le_one_iff`, `FractionalIdeal.finprod_heightOneSpectrum_factorization'`, `FractionalIdeal.mem_inv_iff`, `FractionalIdeal.extended_eq_zero_iff`, `FractionalIdeal.spanSingleton_inv`, `FractionalIdeal.inv_of_ne_zero`, `FractionalIdeal.map_mem_map`, `FractionalIdeal.coe_zero`, `FractionalIdeal.mul_div_self_cancel_iff`, `FractionalIdeal.exists_notMem_one_of_ne_bot`, `FractionalIdeal.map_zero`, `FractionalIdeal.coeIdeal_finprod`, `FractionalIdeal.coe_extended_eq_span`, `FractionalIdeal.coeIdeal_le_coeIdeal`, `FractionalIdeal.absNorm_one`

---

← Back to Index