FundamentalCone

📁 Source: Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

Statistics

Metric	Count
Definitions fundamentalCone, idealSet, idealSetEquiv, idealSetEquivNorm, idealSetMap, instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet, intNorm, integerSet, integerSetEquiv, integerSetEquivNorm, integerSetQuotEquivAssociates, integerSetToAssociates, integerSetTorsionSMul, preimageOfMemIntegerSet, quotIntNorm, instMulActionUnitsRingOfIntegersMixedSpace, instSMulZeroClassUnitsRingOfIntegersMixedSpace, logMap, unitSMul	19
Theorems card_isPrincipal_dvd_norm_le, card_isPrincipal_norm_eq_mul_torsion, existsUnique_preimage_of_mem_integerSet, exists_unitSMul_mem_integerSet, exists_unit_smul_mem, idealSetEquiv_apply, idealSetEquiv_symm_apply, idealSetMap_apply, intNorm_coe, intNorm_idealSetEquiv_apply, integerSetEquivNorm_apply_fst, integerSetEquiv_apply_fst, integerSetQuotEquivAssociates_apply, integerSetToAssociates_apply, integerSetToAssociates_eq_iff, integerSetToAssociates_surjective, integerSetTorsionSMul_smul_coe, integerSetTorsionSMul_stabilizer, mem_idealSet, mem_integerSet, mem_of_normAtPlace_eq, mixedEmbedding_preimageOfMemIntegerSet, ne_zero_of_mem_integerSet, normAtPlace_pos_of_mem, norm_pos_of_mem, preimageOfMemIntegerSet_mixedEmbedding, preimage_of_IdealSetMap, quotIntNorm_apply, smul_mem_iff_mem, smul_mem_of_mem, torsion_smul_mem_of_mem, torsion_unitSMul_mem_integerSet, unit_smul_mem_iff_mem_torsion, logMap_apply, logMap_apply_of_norm_eq_one, logMap_apply_of_norm_one, logMap_eq_logEmbedding, logMap_eq_of_normAtPlace_eq, logMap_mul, logMap_one, logMap_real, logMap_real_smul, logMap_torsion_smul, logMap_unit_smul, logMap_zero, measurableSet_fundamentalCone, norm_unit_smul, unitSMul_smul, unit_smul_eq_iff_mul_eq, unit_smul_eq_zero	50
Total	69

NumberField.mixedEmbedding

Definitions

Name	Category	Theorems
fundamentalCone 📖	CompOp	7 math math: fundamentalCone.mem_normLeOne, fundamentalCone.exists_unit_smul_mem, fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, measurableSet_fundamentalCone, fundamentalCone.mem_idealSet, fundamentalCone.smul_mem_iff_mem, fundamentalCone.mem_integerSet
instMulActionUnitsRingOfIntegersMixedSpace 📖	CompOp	—
instSMulZeroClassUnitsRingOfIntegersMixedSpace 📖	CompOp	—
logMap 📖	CompOp	17 math math: logMap_one, fundamentalCone.logMap_expMapBasis, logMap_real_smul, logMap_eq_of_normAtPlace_eq, logMap_eq_logEmbedding, logMap_apply_of_norm_eq_one, logMap_unit_smul, fundamentalCone.logMap_expMap, logMap_apply, logMap_apply_of_norm_one, logMap_real, logMap_torsion_smul, fundamentalCone.realSpaceToLogSpace_expMap_symm, logMap_zero, logMap_mul, fundamentalCone.logMap_normAtAllPlaces, fundamentalCone.normAtAllPlaces_normLeOne
unitSMul 📖	CompOp	12 math math: norm_unit_smul, fundamentalCone.torsion_unitSMul_mem_integerSet, fundamentalCone.torsion_smul_mem_of_mem, fundamentalCone.integerSetTorsionSMul_smul_coe, unit_smul_eq_iff_mul_eq, fundamentalCone.unit_smul_mem_iff_mem_torsion, fundamentalCone.exists_unitSMul_mem_integerSet, fundamentalCone.exists_unit_smul_mem, logMap_unit_smul, unitSMul_smul, unit_smul_eq_zero, logMap_torsion_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
logMap_apply 📖	mathematical	—	logMap Real Real.instMul Real.instNatCast NumberField.InfinitePlace.mult NumberField.InfinitePlace NumberField.Units.dirichletUnitTheorem.w₀ Real.instSub Real.log DFunLike.coe MonoidWithZeroHom mixedSpace Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace norm Real.instInv Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing NumberField.to_charZero	—	—
logMap_apply_of_norm_eq_one 📖	mathematical	DFunLike.coe MonoidWithZeroHom mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike norm Real.instOne	logMap Real.instMul Real.instNatCast NumberField.InfinitePlace.mult NumberField.Units.dirichletUnitTheorem.w₀ Real.log normAtPlace	—	NumberField.to_charZero logMap_apply Real.log_one MulZeroClass.zero_mul sub_zero
logMap_apply_of_norm_one 📖	mathematical	DFunLike.coe MonoidWithZeroHom mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike norm Real.instOne	logMap Real.instMul Real.instNatCast NumberField.InfinitePlace.mult NumberField.Units.dirichletUnitTheorem.w₀ Real.log normAtPlace	—	logMap_apply_of_norm_eq_one
logMap_eq_logEmbedding 📖	mathematical	—	logMap DFunLike.coe RingHom mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidHom Additive Units NumberField.Units.dirichletUnitTheorem.logSpace AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass NumberField.Units.dirichletUnitTheorem.w₀ AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike NumberField.Units.logEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	NumberField.to_charZero normAtPlace_apply norm_eq_norm NumberField.Units.norm Rat.cast_one Real.log_one MulZeroClass.zero_mul sub_zero
logMap_eq_of_normAtPlace_eq 📖	mathematical	DFunLike.coe MonoidWithZeroHom mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike normAtPlace	logMap	—	NumberField.to_charZero norm_eq_of_normAtPlace_eq
logMap_mul 📖	mathematical	—	logMap mixedSpace Prod.instMul Pi.instMul NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instMul NumberField.InfinitePlace.IsComplex Complex Complex.instMul NumberField.Units.dirichletUnitTheorem.logSpace Pi.instAdd NumberField.Units.dirichletUnitTheorem.w₀ Real.instAdd	—	NumberField.to_charZero map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Real.log_mul norm_ne_zero_iff add_mul Distrib.rightDistribClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt
logMap_one 📖	mathematical	—	logMap mixedSpace Prod.instOne Pi.instOne NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instOne NumberField.InfinitePlace.IsComplex Complex Complex.instOne NumberField.Units.dirichletUnitTheorem.logSpace Pi.instZero NumberField.Units.dirichletUnitTheorem.w₀ Real.instZero	—	NumberField.to_charZero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Real.log_one MulZeroClass.zero_mul sub_self MulZeroClass.mul_zero
logMap_real 📖	mathematical	—	logMap Real mixedSpace Prod.instSMul Function.hasSMul NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id NumberField.InfinitePlace.IsComplex Complex Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike Prod.instOne Pi.instOne Real.instOne Complex.instOne NumberField.Units.dirichletUnitTheorem.logSpace Pi.instZero NumberField.Units.dirichletUnitTheorem.w₀ Real.instZero	—	NumberField.to_charZero logMap_apply normAtPlace_smul norm_smul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass mul_one Real.log_pow mul_comm mul_assoc mul_inv_cancel₀ Nat.cast_ne_zero RCLike.charZero_rclike LT.lt.ne' Module.finrank_pos commRing_strongRankCondition Rat.nontrivial NumberField.to_finiteDimensional Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing sub_self MulZeroClass.mul_zero Pi.zero_apply
logMap_real_smul 📖	mathematical	—	logMap Real mixedSpace Prod.instSMul Function.hasSMul NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id NumberField.InfinitePlace.IsComplex Complex Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike	—	NumberField.to_charZero norm_smul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass mul_one pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass abs_ne_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add smul_one_mul IsScalarTower.right logMap_mul logMap_real zero_add
logMap_torsion_smul 📖	mathematical	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion	logMap mixedSpace unitSMul	—	NumberField.to_charZero map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass norm_eq_norm NumberField.Units.norm Rat.cast_one one_mul normAtPlace_apply NumberField.Units.mem_torsion
logMap_unit_smul 📖	mathematical	—	logMap Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing mixedSpace unitSMul NumberField.Units.dirichletUnitTheorem.logSpace Pi.instAdd NumberField.InfinitePlace NumberField.Units.dirichletUnitTheorem.w₀ Real Real.instAdd DFunLike.coe AddMonoidHom Additive AddZeroClass.toAddZero Additive.addZeroClass Units.instMulOneClass Pi.addZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike NumberField.Units.logEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	unitSMul_smul logMap_mul norm_unit Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_zero logMap_eq_logEmbedding
logMap_zero 📖	mathematical	—	logMap mixedSpace Prod.instZero Pi.instZero NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instZero NumberField.InfinitePlace.IsComplex Complex Complex.instZero NumberField.Units.dirichletUnitTheorem.logSpace NumberField.Units.dirichletUnitTheorem.w₀	—	NumberField.to_charZero map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass Real.log_zero MulZeroClass.zero_mul sub_self MulZeroClass.mul_zero
measurableSet_fundamentalCone 📖	mathematical	—	MeasurableSet mixedSpace Prod.instMeasurableSpace MeasurableSpace.pi NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.measurableSpace NumberField.InfinitePlace.IsComplex Complex Complex.measurableSpace fundamentalCone	—	MeasurableSet.diff Real.instIsStrictOrderedRing instHasSolidNormReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice MeasurableSet.preimage NumberField.to_charZero ZSpan.fundamentalDomain_measurableSet Pi.opensMeasurableSpace Subtype.countable Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_pi_iff Measurable.mul ContinuousMul.measurableMul₂ IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal measurable_const Measurable.sub ContinuousSub.measurableSub₂ IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Measurable.log Continuous.measurable Prod.opensMeasurableSpace secondCountable_of_proper Complex.instProperSpace Complex.borelSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyForallOfCountable continuous_normAtPlace continuous_norm measurableSet_eq_fun instMeasurableEqOfSecondCountableTopologyOfT2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
norm_unit_smul 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom mixedSpace Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike norm Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing unitSMul	—	unitSMul_smul map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass norm_unit one_mul
unitSMul_smul 📖	mathematical	—	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing mixedSpace unitSMul Prod.instMul Pi.instMul NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instMul NumberField.InfinitePlace.IsComplex Complex Complex.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring Real.semiring Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Units.val	—	—
unit_smul_eq_iff_mul_eq 📖	mathematical	—	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing mixedSpace unitSMul DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers.val Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val	—	unitSMul_smul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass NumberField.mixedEmbedding_injective NumberField.RingOfIntegers.coe_eq_algebraMap NumberField.RingOfIntegers.ext_iff
unit_smul_eq_zero 📖	mathematical	—	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing mixedSpace unitSMul Prod.instZero Pi.instZero NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.instZero NumberField.InfinitePlace.IsComplex Complex Complex.instZero	—	Mathlib.Tactic.Contrapose.contrapose₁ exists_normAtPlace_ne_zero_iff unitSMul_smul map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass normAtPlace_apply 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 smul_zero

NumberField.mixedEmbedding.fundamentalCone

Definitions

Name	Category	Theorems
idealSet 📖	CompOp	6 math math: card_isPrincipal_dvd_norm_le, idealSetMap_apply, idealSetEquiv_symm_apply, mem_idealSet, idealSetEquiv_apply, intNorm_idealSetEquiv_apply
idealSetEquiv 📖	CompOp	3 math math: idealSetEquiv_symm_apply, idealSetEquiv_apply, intNorm_idealSetEquiv_apply
idealSetEquivNorm 📖	CompOp	—
idealSetMap 📖	CompOp	2 math math: idealSetMap_apply, preimage_of_IdealSetMap
instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet 📖	CompOp	3 math math: integerSetQuotEquivAssociates_apply, integerSetTorsionSMul_stabilizer, quotIntNorm_apply
intNorm 📖	CompOp	3 math math: quotIntNorm_apply, intNorm_coe, intNorm_idealSetEquiv_apply
integerSet 📖	CompOp	17 math math: integerSetEquivNorm_apply_fst, card_isPrincipal_norm_eq_mul_torsion, integerSetQuotEquivAssociates_apply, integerSetEquiv_apply_fst, integerSetTorsionSMul_smul_coe, integerSetTorsionSMul_stabilizer, exists_unitSMul_mem_integerSet, quotIntNorm_apply, idealSetMap_apply, mixedEmbedding_preimageOfMemIntegerSet, integerSetToAssociates_eq_iff, idealSetEquiv_symm_apply, intNorm_coe, integerSetToAssociates_surjective, idealSetEquiv_apply, mem_integerSet, intNorm_idealSetEquiv_apply
integerSetEquiv 📖	CompOp	1 math math: integerSetEquiv_apply_fst
integerSetEquivNorm 📖	CompOp	1 math math: integerSetEquivNorm_apply_fst
integerSetQuotEquivAssociates 📖	CompOp	1 math math: integerSetQuotEquivAssociates_apply
integerSetToAssociates 📖	CompOp	3 math math: integerSetToAssociates_apply, integerSetToAssociates_eq_iff, integerSetToAssociates_surjective
integerSetTorsionSMul 📖	CompOp	2 math math: integerSetTorsionSMul_smul_coe, integerSetToAssociates_eq_iff
preimageOfMemIntegerSet 📖	CompOp	10 math math: preimageOfMemIntegerSet_mixedEmbedding, integerSetEquivNorm_apply_fst, integerSetQuotEquivAssociates_apply, integerSetEquiv_apply_fst, integerSetToAssociates_apply, mixedEmbedding_preimageOfMemIntegerSet, idealSetEquiv_symm_apply, preimage_of_IdealSetMap, idealSetEquiv_apply, intNorm_idealSetEquiv_apply
quotIntNorm 📖	CompOp	1 math math: quotIntNorm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_isPrincipal_dvd_norm_le 📖	mathematical	—	Nat.card Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Submodule.instNonUnitalSemiring Semiring.toModule IsScalarTower.right Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Real Real.instLE Real.instNatCast DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt NumberField.Units.torsionOrder Set.Elem NumberField.mixedEmbedding.mixedSpace idealSet Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring NumberField.mixedEmbedding.norm Set Set.instMembership	—	IsScalarTower.right NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt le_or_gt Real.instIsStrictOrderedRing Nat.le_floor_iff NumberField.Units.torsionOrder.eq_1 Nat.card_eq_fintype_card Nat.card_prod Nat.card_congr Finset.mem_Iic Subtype.prop RCLike.charZero_rclike lt_iff_not_ge lt_of_lt_of_le Nat.cast_nonneg Real.instIsOrderedRing NumberField.mixedEmbedding.norm_nonneg Nat.card_of_isEmpty Subtype.isEmpty_false MulZeroClass.zero_mul
card_isPrincipal_norm_eq_mul_torsion 📖	mathematical	—	Nat.card Set.Elem Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors setOf Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt NumberField.Units.torsionOrder NumberField.mixedEmbedding.mixedSpace integerSet Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring NumberField.mixedEmbedding.norm Set Set.instMembership Real.instNatCast	—	NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt NumberField.Units.torsionOrder.eq_1 Nat.card_eq_fintype_card Nat.card_prod Nat.card_congr
existsUnique_preimage_of_mem_integerSet 📖	mathematical	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership integerSet	ExistsUnique NumberField.RingOfIntegers DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers.val	—	mem_integerSet Function.Injective.existsUnique_of_mem_range NumberField.mixedEmbedding_injective NumberField.RingOfIntegers.coe_injective Set.mem_range_self
exists_unitSMul_mem_integerSet 📖	mathematical	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding Set.range NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing algebraMap NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring	integerSet Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero NumberField.mixedEmbedding.unitSMul	—	Iff.not NumberField.mixedEmbedding.norm_eq_zero_iff' Set.mem_range_of_mem_image exists_unit_smul_mem mem_integerSet NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
exists_unit_smul_mem 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NumberField.mixedEmbedding.unitSMul	—	Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice ZSpan.exist_unique_vadd_mem_fundamentalDomain Module.Basis.ofZLatticeBasis_span Set.mem_preimage NumberField.mixedEmbedding.logMap_unit_smul map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass NumberField.to_charZero NumberField.mixedEmbedding.norm_eq_norm NumberField.Units.norm Rat.cast_one one_mul
idealSetEquiv_apply 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership integerSet Set.Elem setOf NumberField.RingOfIntegers SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors preimageOfMemIntegerSet DFunLike.coe Equiv idealSet EquivLike.toFunLike Equiv.instEquivLike idealSetEquiv	—	—
idealSetEquiv_symm_apply 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership idealSet DFunLike.coe Equiv Set.Elem integerSet setOf NumberField.RingOfIntegers SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors preimageOfMemIntegerSet EquivLike.toFunLike Equiv.instEquivLike Equiv.symm idealSetEquiv	—	idealSetEquiv_apply Equiv.apply_symm_apply
idealSetMap_apply 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership integerSet idealSetMap idealSet	—	—
intNorm_coe 📖	mathematical	—	Real Real.instNatCast intNorm DFunLike.coe MonoidWithZeroHom NumberField.mixedEmbedding.mixedSpace Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.norm Set Set.instMembership integerSet	—	intNorm.eq_1 Nat.cast_natAbs Rat.cast_intCast Int.cast_abs Rat.instIsStrictOrderedRing NumberField.to_charZero Algebra.coe_norm_int NumberField.mixedEmbedding.norm_eq_norm mixedEmbedding_preimageOfMemIntegerSet
intNorm_idealSetEquiv_apply 📖	mathematical	—	Real Real.instNatCast intNorm Set.Elem NumberField.mixedEmbedding.mixedSpace integerSet Set Set.instMembership setOf NumberField.RingOfIntegers SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors preimageOfMemIntegerSet DFunLike.coe Equiv idealSet EquivLike.toFunLike Equiv.instEquivLike idealSetEquiv MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.norm	—	intNorm_coe idealSetEquiv_apply
integerSetEquivNorm_apply_fst 📖	mathematical	—	Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt Units MonoidWithZero.toMonoid Subgroup Units.instGroup Subgroup.instSetLike NumberField.Units.torsion Equiv Set.Elem NumberField.mixedEmbedding.mixedSpace integerSet Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring NumberField.mixedEmbedding.norm Set Set.instMembership Real.instNatCast EquivLike.toFunLike Equiv.instEquivLike integerSetEquivNorm Ideal.span Set.instSingletonSet preimageOfMemIntegerSet	—	NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt
integerSetEquiv_apply_fst 📖	mathematical	—	Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Units MonoidWithZero.toMonoid Subgroup Units.instGroup Subgroup.instSetLike NumberField.Units.torsion DFunLike.coe Equiv Set.Elem NumberField.mixedEmbedding.mixedSpace integerSet EquivLike.toFunLike Equiv.instEquivLike integerSetEquiv Ideal.span Set Set.instSingletonSet preimageOfMemIntegerSet	—	—
integerSetQuotEquivAssociates_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem NumberField.mixedEmbedding.mixedSpace integerSet MulAction.orbitRel Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Subgroup.toGroup instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet Associates Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Submonoid.instSetLike nonZeroDivisors Submonoid.toMonoid EquivLike.toFunLike Equiv.instEquivLike integerSetQuotEquivAssociates Associated.setoid preimageOfMemIntegerSet	—	—
integerSetToAssociates_apply 📖	mathematical	—	integerSetToAssociates NumberField.RingOfIntegers Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Associated.setoid Submonoid.toMonoid MonoidWithZero.toMonoid preimageOfMemIntegerSet	—	—
integerSetToAssociates_eq_iff 📖	mathematical	—	integerSetToAssociates Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Set.Elem NumberField.mixedEmbedding.mixedSpace integerSet integerSetTorsionSMul	—	SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_comm NumberField.mixedEmbedding_injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mixedEmbedding_preimageOfMemIntegerSet unit_smul_mem_iff_mem_torsion Subtype.prop
integerSetToAssociates_surjective 📖	mathematical	—	Set.Elem NumberField.mixedEmbedding.mixedSpace integerSet Associates NumberField.RingOfIntegers Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Submonoid.toMonoid MonoidWithZero.toMonoid integerSetToAssociates	—	exists_unitSMul_mem_integerSet map_ne_zero NumberField.mixedEmbedding.instNontrivialMixedSpace RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass NumberField.RingOfIntegers.coe_ne_zero_iff nonZeroDivisors.coe_ne_zero NumberField.RingOfIntegers.instNontrivial Set.mem_range_self NumberField.mixedEmbedding_injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mixedEmbedding_preimageOfMemIntegerSet mul_comm map_inv MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Units.mul_inv_cancel_right
integerSetTorsionSMul_smul_coe 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership integerSet Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Set.Elem integerSetTorsionSMul NumberField.mixedEmbedding.unitSMul	—	—
integerSetTorsionSMul_stabilizer 📖	mathematical	—	MulAction.stabilizer Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Set.Elem NumberField.mixedEmbedding.mixedSpace integerSet Subgroup.toGroup instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet Bot.bot Subgroup.instBot	—	Subgroup.eq_bot_iff_forall SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass OneMemClass.coe_eq_one Units.val_eq_one mul_eq_right₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain nonZeroDivisors.coe_ne_zero NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.ext_iff map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass NumberField.mixedEmbedding_injective mixedEmbedding_preimageOfMemIntegerSet NumberField.mixedEmbedding.unitSMul_smul integerSetTorsionSMul_smul_coe MulAction.mem_stabilizer_iff
mem_idealSet 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership idealSet NumberField.mixedEmbedding.fundamentalCone NumberField.RingOfIntegers SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors DFunLike.coe RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers.val	—	NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsDomain RingHomSurjective.ids
mem_integerSet 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership integerSet NumberField.mixedEmbedding.fundamentalCone DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers.val	—	—
mem_of_normAtPlace_eq 📖	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone DFunLike.coe MonoidWithZeroHom Real Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.normAtPlace	—	—	Real.instIsStrictOrderedRing instHasSolidNormReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice Set.mem_preimage NumberField.mixedEmbedding.logMap_eq_of_normAtPlace_eq NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq
mixedEmbedding_preimageOfMemIntegerSet 📖	mathematical	—	DFunLike.coe RingHom NumberField.mixedEmbedding.mixedSpace Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers.val NumberField.RingOfIntegers Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing SetLike.instMembership Submonoid.instSetLike nonZeroDivisors preimageOfMemIntegerSet Set Set.instMembership integerSet	—	preimageOfMemIntegerSet.eq_1 mem_integerSet Subtype.prop
ne_zero_of_mem_integerSet 📖	—	—	—	—	Real.instIsStrictOrderedRing instHasSolidNormReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice Subtype.prop ZeroHom.map_zero'
normAtPlace_pos_of_mem 📖	mathematical	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone	Real Real.instLT Real.instZero DFunLike.coe MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.normAtPlace	—	lt_of_le_of_ne NumberField.mixedEmbedding.normAtPlace_nonneg NumberField.mixedEmbedding.norm_ne_zero_iff LT.lt.ne' norm_pos_of_mem
norm_pos_of_mem 📖	mathematical	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone	Real Real.instLT Real.instZero DFunLike.coe MonoidWithZeroHom Prod.instMulZeroOneClass Pi.mulZeroOneClass NumberField.InfinitePlace NumberField.InfinitePlace.IsReal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring MonoidWithZeroHom.funLike NumberField.mixedEmbedding.norm	—	lt_of_le_of_ne NumberField.mixedEmbedding.norm_nonneg Real.instIsStrictOrderedRing instHasSolidNormReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice
preimageOfMemIntegerSet_mixedEmbedding 📖	mathematical	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership integerSet DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Prod.instNonAssocSemiring Pi.nonAssocSemiring NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Real Real.semiring NumberField.InfinitePlace.IsComplex Complex Complex.instSemiring RingHom.instFunLike NumberField.mixedEmbedding NumberField.RingOfIntegers.val	NumberField.RingOfIntegers Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing SetLike.instMembership Submonoid.instSetLike nonZeroDivisors preimageOfMemIntegerSet	—	NumberField.mixedEmbedding_injective mixedEmbedding_preimageOfMemIntegerSet
preimage_of_IdealSetMap 📖	mathematical	—	NumberField.RingOfIntegers Set Set.instMembership SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id SetLike.instMembership Submonoid.instSetLike nonZeroDivisors preimageOfMemIntegerSet idealSetMap	—	mem_idealSet Subtype.prop preimageOfMemIntegerSet_mixedEmbedding
quotIntNorm_apply 📖	mathematical	—	quotIntNorm Set.Elem NumberField.mixedEmbedding.mixedSpace integerSet MulAction.orbitRel Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion Subgroup.toGroup instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet intNorm	—	—
smul_mem_iff_mem 📖	mathematical	—	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone Real Prod.instSMul Function.hasSMul NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id NumberField.InfinitePlace.IsComplex Complex Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike	—	eq_inv_smul_iff₀ smul_mem_of_mem inv_ne_zero
smul_mem_of_mem 📖	mathematical	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone	Real Prod.instSMul Function.hasSMul NumberField.InfinitePlace NumberField.InfinitePlace.IsReal Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id NumberField.InfinitePlace.IsComplex Complex Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike	—	Real.instIsStrictOrderedRing instHasSolidNormReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice Set.mem_preimage NumberField.mixedEmbedding.logMap_real_smul Set.mem_setOf_eq NumberField.to_charZero NumberField.mixedEmbedding.norm_smul mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass pow_ne_zero isReduced_of_noZeroDivisors abs_ne_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
torsion_smul_mem_of_mem 📖	mathematical	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion	NumberField.mixedEmbedding.unitSMul	—	Real.instIsStrictOrderedRing instHasSolidNormReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice Set.mem_preimage NumberField.mixedEmbedding.logMap_torsion_smul Set.mem_setOf_eq NumberField.mixedEmbedding.unitSMul_smul map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass NumberField.mixedEmbedding.norm_unit one_mul
torsion_unitSMul_mem_integerSet 📖	mathematical	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion NumberField.mixedEmbedding.mixedSpace Set Set.instMembership integerSet	NumberField.mixedEmbedding.unitSMul	—	mem_integerSet torsion_smul_mem_of_mem map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
unit_smul_mem_iff_mem_torsion 📖	mathematical	NumberField.mixedEmbedding.mixedSpace Set Set.instMembership NumberField.mixedEmbedding.fundamentalCone	Units NumberField.RingOfIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NumberField.mixedEmbedding.unitSMul Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike NumberField.Units.torsion	—	NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff Real.instIsStrictOrderedRing instHasSolidNormReal FiniteDimensional.finiteDimensional_pi' Subtype.finite Finite.of_fintype FiniteDimensional.rclike_to_real pi_properSpace instProperSpaceReal NumberField.Units.instDiscrete_unitLattice NumberField.Units.instZLattice_unitLattice Module.Basis.ofZLatticeBasis_span Submodule.zero_mem ExistsUnique.unique ZSpan.exist_unique_vadd_mem_fundamentalDomain AddSubmonoid.mk_vadd vadd_eq_add NumberField.mixedEmbedding.logMap_unit_smul zero_add torsion_smul_mem_of_mem

---

← Back to Index