Different

📁 Source: Mathlib/RingTheory/DedekindDomain/Different.lean

Statistics

Metric	Count
Definitions `dual`, `traceDual`, `differentIdeal`	3
Theorems `coe_dual`, `coe_dual_one`, `dual_div_dual`, `dual_dual`, `dual_eq_dual_mul_dual`, `dual_eq_mul_inv`, `dual_eq_zero_iff`, `dual_injective`, `dual_inv`, `dual_inv_le`, `dual_involutive`, `dual_le_dual`, `dual_mul_self`, `dual_ne_zero`, `dual_ne_zero_iff`, `dual_zero`, `inv_le_dual`, `le_dual_iff`, `le_dual_inv_aux`, `mem_dual`, `one_le_dual_one`, `self_mul_dual`, `smul_mem_dual_one`, `trace_mem_dual_one`, `le_traceDual`, `le_traceDual_comm`, `le_traceDual_iff_map_le_one`, `le_traceDual_mul_iff`, `le_traceDual_traceDual`, `mem_traceDual`, `mem_traceDual_iff_isIntegral`, `one_le_traceDual_one`, `restrictScalars_traceDual`, `traceDual_bot`, `traceDual_span_of_basis`, `traceDual_top`, `traceDual_top'`, `aeval_derivative_mem_differentIdeal`, `coeIdeal_differentIdeal`, `coeSubmodule_differentIdeal`, `coeSubmodule_differentIdeal_fractionRing`, `conductor_mul_differentIdeal`, `differentIdeal_eq_differentIdeal_mul_differentIdeal`, `differentIdeal_ne_bot`, `differentialIdeal_le_fractionalIdeal_iff`, `differentialIdeal_le_iff`, `dvd_differentIdeal_iff`, `dvd_differentIdeal_of_not_isSeparable`, `isIntegral_discr_mul_of_mem_traceDual`, `map_equiv_traceDual`, `not_dvd_differentIdeal_iff`, `not_dvd_differentIdeal_of_intTrace_not_mem`, `not_dvd_differentIdeal_of_isCoprime`, `not_dvd_differentIdeal_of_isCoprime_of_isSeparable`, `pow_sub_one_dvd_differentIdeal`, `pow_sub_one_dvd_differentIdeal_aux`, `traceForm_dualSubmodule_adjoin`	57
Total	60

FractionalIdeal

Definitions

Name	Category	Theorems
`dual` 📖	CompOp	21 math math: `le_dual_iff`, `dual_eq_dual_mul_dual`, `one_le_dual_one`, `coe_dual`, `coe_dual_one`, `coeIdeal_differentIdeal`, `inv_le_dual`, `dual_mul_self`, `mem_dual`, `dual_involutive`, `dual_eq_mul_inv`, `dual_div_dual`, `dual_zero`, `dual_le_dual`, `dual_inv`, `dual_eq_zero_iff`, `dual_inv_le`, `dual_injective`, `self_mul_dual`, `dual_dual`, `le_dual_inv_aux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_dual` 📖	mathematical	—	`coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `Submodule.traceDual`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual.eq_1`
`coe_dual_one` 📖	mathematical	—	`coeToSubmodule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `FractionalIdeal` `instOne` `Submodule.traceDual` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule.one`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `coe_one` `coe_dual` `one_ne_zero` `NeZero.one` `instNontrivialNonZeroDivisors`
`dual_div_dual` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instDivNonZeroDivisors` `IsDedekindDomain.toIsDomain` `dual` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors`	—	`IsDedekindDomain.toIsDomain` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `dual_eq_mul_inv` `mul_div_mul_comm` `div_self` `NeZero.one` `instNontrivialNonZeroDivisors` `one_mul` `inv_div_inv`
`dual_dual` 📖	mathematical	—	`dual` `IsDomain.toNontrivial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual_eq_mul_inv` `mul_inv` `inv_inv` `mul_assoc` `mul_inv_cancel₀` `dual_ne_zero_iff` `one_ne_zero` `NeZero.one` `instNontrivialNonZeroDivisors` `one_mul`
`dual_eq_dual_mul_dual` 📖	mathematical	—	`dual` `IsDomain.toNontrivial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instOne` `instMul` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `extendedHomₐ`	—	`IsIntegralClosure.isLocalization` `IsDedekindDomain.toIsDomain` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `nonZeroDivisors_le_comap_nonZeroDivisors_of_injective` `IsDomain.to_noZeroDivisors` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsLocalization.algebraMap_apply_eq_map_map_submonoid` `le_antisymm` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `spanSingleton_le_iff_mem` `mul_inv_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `instMulPosReflectLENonZeroDivisors` `bot_lt_iff_ne_bot` `instNontrivialNonZeroDivisors` `NeZero.one` `map_inv₀` `coe_le_coe` `extendedHom_apply` `IsScalarTower.right` `coe_mul` `coe_spanSingleton` `coe_extended_eq_span` `coe_dual_one` `Submodule.span_mul_span` `Submodule.span_le` `Algebra.to_smulCommClass` `mul_comm` `Algebra.smul_def` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `mul_one` `coe_one` `mem_inv_iff` `trace_mem_dual_one` `Submodule.smul_mem` `Submodule.span_eq` `smul_mem_dual_one`
`dual_eq_mul_inv` 📖	mathematical	—	`dual` `IsDomain.toNontrivial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `instOne` `instInvNonZeroDivisors`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual.congr_simp` `dual_zero` `inv_zero` `MulZeroClass.mul_zero` `le_antisymm` `le_mul_inv_iff₀` `MulPosReflectLE.toMulPosReflectLT` `instMulPosReflectLENonZeroDivisors` `pos_iff_ne_zero` `instCanonicallyOrderedAdd` `le_dual_iff` `le_refl` `mul_assoc` `inv_mul_cancel₀` `mul_one`
`dual_eq_zero_iff` 📖	mathematical	—	`dual` `IsDomain.toNontrivial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instZero`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `not_imp_not` `dual_ne_zero` `dual_zero`
`dual_injective` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors`	—	`Function.Involutive.injective` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual_involutive`
`dual_inv` 📖	mathematical	—	`dual` `IsDomain.toNontrivial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instInvNonZeroDivisors` `instMul` `instOne`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual_eq_mul_inv` `inv_inv`
`dual_inv_le` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain` `dual` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors`	—	`IsDedekindDomain.toIsDomain` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `dual.congr_simp` `dual_zero` `inv_zero` `inv_le_comm₀` `PosMulReflectLE.toPosMulReflectLT` `instPosMulReflectLENonZeroDivisors` `MulPosReflectLE.toMulPosReflectLT` `instMulPosReflectLENonZeroDivisors` `instCanonicallyOrderedAdd` `inv_le_dual`
`dual_involutive` 📖	mathematical	—	`Function.Involutive` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors`	—	`dual_dual`
`dual_le_dual` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual_dual` `le_dual_iff` `dual_ne_zero_iff` `mul_comm`
`dual_mul_self` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `instOne`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual_eq_mul_inv` `mul_assoc` `inv_mul_cancel₀` `mul_one`
`dual_ne_zero` 📖	—	—	—	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `Subtype.prop` `mem_dual` `IsIntegrallyClosed.isIntegral_iff` `Algebra.isIntegral_trace` `IsIntegralClosure.isIntegral_iff` `Algebra.smul_def` `mem_nonZeroDivisors_iff_ne_zero` `IsIntegralClosure.algebraMap_injective` `RingHom.map_zero` `mem_zero_iff`
`dual_ne_zero_iff` 📖	—	—	—	—	`Iff.not` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual_eq_zero_iff`
`dual_zero` 📖	mathematical	—	`dual` `IsDomain.toNontrivial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instZero`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual.eq_1`
`inv_le_dual` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain` `dual` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors`	—	`IsDedekindDomain.toIsDomain` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `inv_zero` `dual.congr_simp` `dual_zero` `le_dual_inv_aux` `le_of_eq` `mul_inv_cancel₀`
`le_dual_iff` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `instMul` `instOne`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `instCanonicallyOrderedAdd` `MulZeroClass.zero_mul` `coe_le_coe` `IsScalarTower.right` `coe_mul` `coe_dual` `coe_dual_one` `Submodule.le_traceDual`
`le_dual_inv_aux` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instMul` `instOne`	`dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual.eq_1` `Submodule.mem_one` `IsIntegrallyClosed.isIntegral_iff` `Algebra.isIntegral_trace` `IsIntegralClosure.isIntegral_iff` `mul_mem_mul` `mul_comm`
`mem_dual` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `instSetLike` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `Subring.instSetLike` `RingHom.range` `CommRing.toRing` `algebraMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.traceForm`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `dual.eq_1` `Submodule.mem_one`
`one_le_dual_one` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOne` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors`	—	`le_dual_inv_aux` `one_ne_zero` `NeZero.one` `instNontrivialNonZeroDivisors` `one_mul` `le_refl`
`self_mul_dual` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `instOne`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `mul_comm` `dual_mul_self`
`smul_mem_dual_one` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `instSetLike` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `instOne` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr`	`Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `NeZero.one` `instNontrivialNonZeroDivisors` `mul_comm` `Algebra.smul_def` `LinearMap.map_smul` `SMulCommClass.smul_comm` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `Algebra.trace_trace` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`trace_mem_dual_one` 📖	mathematical	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `instSetLike` `dual` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `instOne`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semiring.toModule` `LinearMap.instFunLike` `Algebra.trace`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDomain.to_noZeroDivisors` `NeZero.one` `instNontrivialNonZeroDivisors` `mul_comm` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `Algebra.trace_trace` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `algebraMap_smul`

Submodule

Definitions

Name	Category	Theorems
`traceDual` 📖	CompOp	20 math math: `one_le_traceDual_one`, `coeSubmodule_differentIdeal`, `coeSubmodule_differentIdeal_fractionRing`, `traceDual_top'`, `le_traceDual_traceDual`, `FractionalIdeal.coe_dual`, `FractionalIdeal.coe_dual_one`, `traceDual_le_span_map_traceDual`, `map_equiv_traceDual`, `restrictScalars_traceDual`, `le_traceDual`, `le_traceDual_comm`, `traceDual_eq_span_map_traceDual_of_linearDisjoint`, `mem_traceDual`, `traceDual_bot`, `traceDual_span_of_basis`, `le_traceDual_mul_iff`, `le_traceDual_iff_map_le_one`, `traceDual_top`, `mem_traceDual_iff_isIntegral`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_traceDual` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `traceDual` `mul` `IsScalarTower.right` `one`	—	`IsScalarTower.right` `le_traceDual_mul_iff` `mul_one`
`le_traceDual_comm` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `traceDual`	—	`IsScalarTower.right` `le_traceDual` `mul_comm`
`le_traceDual_iff_map_le_one` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `traceDual` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.restrictScalars` `Semiring.toModule` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.right` `Algebra.trace` `restrictScalars` `mul` `one`	—	`RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `map_le_iff_le_comap` `restrictScalars_mul` `mul_le` `instIsConcreteLE`
`le_traceDual_mul_iff` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `traceDual` `mul` `IsScalarTower.right`	—	`IsScalarTower.right` `RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `map.congr_simp` `restrictScalars.congr_simp` `mul_assoc`
`le_traceDual_traceDual` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `traceDual`	—	`le_traceDual_comm` `le_rfl`
`mem_traceDual` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `setLike` `traceDual` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `Subring.instSetLike` `RingHom.range` `CommRing.toRing` `algebraMap` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.traceForm`	—	`mem_one`
`mem_traceDual_iff_isIntegral` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `setLike` `traceDual` `IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.traceForm`	—	`mem_one` `IsIntegrallyClosed.isIntegral_iff`
`one_le_traceDual_one` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `one` `traceDual`	—	`RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `le_traceDual_iff_map_le_one` `mul_one` `one_eq_range` `mem_one` `IsIntegrallyClosed.isIntegral_iff` `Algebra.isIntegral_trace` `IsIntegralClosure.isIntegral_iff`
`restrictScalars_traceDual` 📖	mathematical	—	`restrictScalars` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.toSMul` `traceDual` `LinearMap.BilinForm.dualSubmodule` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.traceForm`	—	—
`traceDual_bot` 📖	mathematical	—	`traceDual` `Bot.bot` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instBot` `Top.top` `instTop`	—	`ext` `MulZeroClass.mul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`
`traceDual_span_of_basis` 📖	mathematical	`restrictScalars` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.toSMul` `span` `Set.range` `DFunLike.coe` `Module.Basis` `Semifield.toCommSemiring` `Module.Basis.instFunLike`	`traceDual` `Field.toCommRing` `Module.Basis.traceDual`	—	`restrictScalars_traceDual` `LinearMap.BilinForm.dualSubmodule_span_of_basis` `traceForm_nondegenerate`
`traceDual_top` 📖	mathematical	—	`traceDual` `Top.top` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instTop` `IsField` `Bot.bot` `instBot`	—	`IsScalarTower.right` `RingHomSurjective.ids` `IsFractionRing.surjective_iff_isField` `LinearMap.range_eq_top` `Algebra.trace_surjective` `RingHom.range_eq_top` `eq_top_iff` `instIsConcreteLE` `traceDual_top'`
`traceDual_top'` 📖	mathematical	—	`traceDual` `Top.top` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `restrictScalars` `Semiring.toModule` `Algebra.toSMul` `IsScalarTower.right` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Algebra.trace` `one` `Bot.bot` `instBot`	—	`IsScalarTower.right` `RingHomSurjective.ids` `eq_top_iff` `instIsConcreteLE` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `mul_inv_cancel_left₀`

(root)

Definitions

Name	Category	Theorems
`differentIdeal` 📖	CompOp	21 math math: `IsDedekindDomain.differentIdeal_dvd_map_differentIdeal`, `NumberField.isCoprime_differentIdeal_of_isCoprime_discr`, `differentIdeal_eq_differentIdeal_mul_differentIdeal`, `pow_sub_one_dvd_differentIdeal`, `coeSubmodule_differentIdeal`, `coeSubmodule_differentIdeal_fractionRing`, `differentialIdeal_le_iff`, `NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow`, `coeIdeal_differentIdeal`, `differentialIdeal_le_fractionalIdeal_iff`, `not_dvd_differentIdeal_of_isCoprime_of_isSeparable`, `dvd_differentIdeal_iff`, `NumberField.discr_mem_differentIdeal`, `NumberField.absNorm_differentIdeal`, `dvd_differentIdeal_of_not_isSeparable`, `not_dvd_differentIdeal_of_isCoprime`, `not_dvd_differentIdeal_iff`, `aeval_derivative_mem_differentIdeal`, `conductor_mul_differentIdeal`, `not_dvd_differentIdeal_of_intTrace_not_mem`, `pow_sub_one_dvd_differentIdeal_aux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_derivative_mem_differentIdeal` 📖	mathematical	`Algebra.adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Set` `Set.instSingletonSet` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `differentIdeal` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `LinearMap` `RingHom.id` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.derivative` `minpoly` `CommRing.toRing`	—	`SetLike.le_def` `instIsConcreteLE` `IsScalarTower.right` `conductor_mul_differentIdeal` `Ideal.mul_le_left` `Ideal.mem_span_singleton_self`
`coeIdeal_differentIdeal` 📖	mathematical	—	`FractionalIdeal.coeIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `differentIdeal` `FractionalIdeal` `FractionalIdeal.instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain` `FractionalIdeal.dual` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `FractionalIdeal.instOne`	—	`FractionalIdeal.coeToSubmodule_injective` `IsDedekindDomain.toIsDomain` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `coeSubmodule_differentIdeal` `inv_eq_one_div` `FractionalIdeal.coe_div` `FractionalIdeal.dual_ne_zero` `one_ne_zero` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors` `FractionalIdeal.coe_one` `FractionalIdeal.coe_dual_one`
`coeSubmodule_differentIdeal` 📖	mathematical	—	`IsLocalization.coeSubmodule` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `differentIdeal` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule.instDiv` `Submodule.one` `Submodule.traceDual`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.ext_ring` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IsLocalization.coeSubmodule.eq_1` `IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `IsLocalization.ringHom_ext` `RingHom.ext` `AlgEquiv.commutes` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `IsScalarTower.algebraMap_apply` `Algebra.IsSeparable.of_equiv_equiv` `IsDomain.to_noZeroDivisors` `Module.Finite.of_equiv_equiv` `IsIntegralClosure.isIntegral_algebra` `RingHomSurjective.ids` `Submodule.map_comp` `coeSubmodule_differentIdeal_fractionRing` `Submodule.map_div` `AlgEquiv.toAlgHom_toLinearMap` `Submodule.map_one` `map_equiv_traceDual` `Submodule.ext`
`coeSubmodule_differentIdeal_fractionRing` 📖	mathematical	—	`IsLocalization.coeSubmodule` `CommRing.toCommSemiring` `FractionRing` `OreLocalization.instCommSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAlgebra` `Algebra.id` `differentIdeal` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `FractionRing.field` `IsDedekindDomain.toIsDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule.instDiv` `Submodule.one` `Submodule.traceDual` `FractionRing.liftAlgebra` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `CommRing.toRing` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `FractionRing.instIsScalarTower` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IsScalarTower.right` `Algebra.toSMul` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `IsLocalization.coeSubmodule.eq_1` `differentIdeal.eq_1` `Submodule.map_comap_eq` `inf_eq_right` `Localization.isLocalization` `IsIntegralClosure.of_isIntegrallyClosed` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `FractionalIdeal.dual_inv_le` `RingHomSurjective.ids` `Submodule.one_eq_range` `Submodule.traceDual.congr_simp` `FractionalIdeal.coe_one` `FractionalIdeal.coe_dual` `one_ne_zero` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors` `FractionalIdeal.coe_div` `FractionalIdeal.dual_ne_zero` `one_div`
`conductor_mul_differentIdeal` 📖	mathematical	`Algebra.adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Set` `Set.instSingletonSet` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Ideal` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `conductor` `differentIdeal` `Ideal.span` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.aeval` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.derivative` `minpoly` `CommRing.toRing`	—	`IsIntegralClosure.isIntegral` `FractionalIdeal.coeIdeal_injective` `IsIntegralClosure.isFractionRing_of_finite_extension` `IsDedekindDomain.toIsDomain` `IsScalarTower.right` `FractionalIdeal.coeIdeal_mul` `FractionalIdeal.coeIdeal_span_singleton` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `coeIdeal_differentIdeal` `mul_inv_eq_iff_eq_mul₀` `FractionalIdeal.dual_ne_zero` `one_ne_zero` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors` `FractionalIdeal.coeToSubmodule_injective` `IsScalarTower.to_smulCommClass'` `FractionalIdeal.coe_mul` `FractionalIdeal.coe_spanSingleton` `Submodule.span_singleton_mul` `Submodule.ext` `Polynomial.Separable.aeval_derivative_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsSeparable.isSeparable` `minpoly.aeval` `Polynomial.aeval_algebraMap_apply` `Polynomial.aeval_map_algebraMap` `Polynomial.derivative_map` `minpoly.isIntegrallyClosed_eq_field_fractions` `Submodule.mem_smul_iff_inv_mul_mem` `FractionalIdeal.mem_coe` `FractionalIdeal.mem_dual` `mem_coeSubmodule_conductor` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `IsDomain.toIsCancelMulZero` `instIsDomain` `inv_eq_zero` `IsIntegral.map` `IsScalarTower.left` `AlgHom.algHomClass` `Submodule.mul_mem_smul_iff` `mem_nonZeroDivisors_of_ne_zero` `traceForm_dualSubmodule_adjoin` `mul_assoc` `RingHomSurjective.ids` `Submodule.one_eq_range` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `mul_one`
`differentIdeal_eq_differentIdeal_mul_differentIdeal` 📖	mathematical	—	`differentIdeal` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `Algebra.isSeparable_tower_top_of_isSeparable` `FractionRing.instIsScalarTower_1` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `Algebra.isSeparable_tower_bot_of_isSeparable` `FractionRing.instNontrivial` `Localization.isLocalization` `FractionalIdeal.coeIdeal_mul` `IsScalarTower.left` `Module.Finite.of_isLocalization` `Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors` `Algebra.IsAlgebraic.of_finite` `IsDomain.to_noZeroDivisors` `IsIntegralClosure.of_isIntegrallyClosed` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Algebra.IsIntegral.of_finite` `coeIdeal_differentIdeal` `FractionalIdeal.extendedHomₐ_coeIdeal_eq_map` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_inv` `inv_eq_iff_eq_inv` `inv_inv` `FractionalIdeal.dual_eq_dual_mul_dual`
`differentIdeal_ne_bot` 📖	—	—	—	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `Localization.isLocalization` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `instFiniteDimensionalFractionRingOfFinite` `IsIntegralClosure.of_isIntegrallyClosed` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Algebra.IsIntegral.of_finite` `IsDomain.to_noZeroDivisors` `coeIdeal_differentIdeal` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors`
`differentialIdeal_le_fractionalIdeal_iff` 📖	mathematical	—	`FractionalIdeal` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `FractionalIdeal.instPartialOrder` `FractionalIdeal.coeIdeal` `differentIdeal` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule.instPartialOrder` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.restrictScalars` `Semiring.toModule` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.right` `Algebra.trace` `Submodule.restrictScalars` `FractionalIdeal.coeToSubmodule` `FractionalIdeal.instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain` `Submodule.one`	—	`RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `IsDedekindDomain.toIsDomain` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `coeIdeal_differentIdeal` `FractionalIdeal.inv_le_comm` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors` `FractionalIdeal.coe_le_coe` `FractionalIdeal.coe_dual_one` `Submodule.le_traceDual_iff_map_le_one` `Submodule.map.congr_simp` `Submodule.restrictScalars.congr_simp` `mul_one`
`differentialIdeal_le_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `differentIdeal` `Submodule` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule.map` `RingHom.id` `RingHomSurjective.ids` `LinearMap.restrictScalars` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.right` `Algebra.trace` `Submodule.restrictScalars` `FractionalIdeal.coeToSubmodule` `nonZeroDivisors` `FractionalIdeal` `FractionalIdeal.instInvNonZeroDivisors` `IsDedekindDomain.toIsDomain` `FractionalIdeal.coeIdeal` `Submodule.one`	—	`RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `IsDedekindDomain.toIsDomain` `FractionalIdeal.coeIdeal_le_coeIdeal` `differentialIdeal_le_fractionalIdeal_iff`
`dvd_differentIdeal_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `differentIdeal` `Algebra.IsUnramifiedAt`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsScalarTower.right` `iff_not_comm` `not_dvd_differentIdeal_iff`
`dvd_differentIdeal_of_not_isSeparable` 📖	mathematical	`Algebra.IsSeparable` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commRing` `Ideal.Quotient.instRingQuotient` `Ideal.Quotient.algebraOfLiesOver`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `differentIdeal`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsScalarTower.right` `Ideal.dvd_iff_le` `Ideal.map_le_iff_le_comap` `Eq.le` `Ideal.LiesOver.over` `pow_one` `pow_sub_one_dvd_differentIdeal` `pow_two` `mul_dvd_mul_left` `Iff.not` `Ideal.map_eq_bot_iff_of_injective` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Submodule.mul_bot` `IsScalarTower.left` `Ideal.bot_mul` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq_zero_iff_mem` `Algebra.trace_quotient_eq_of_isDedekindDomain` `mul_comm` `IsScalarTower.of_algebraMap_eq'` `Module.Finite.of_restrictScalars_finite` `Module.Finite.quotient` `Ideal.prime_iff_isPrime` `Ideal.IsMaximal.isPrime'` `Ideal.isCoprime_iff_gcd` `Irreducible.gcd_eq_one_iff` `Prime.irreducible` `Ideal.isCancelMulZero` `RingEquiv.map_mul'` `RingEquiv.map_add'` `Ideal.quotientMulEquivQuotientProd_snd` `Algebra.trace_eq_of_algEquiv` `Algebra.trace_prod_apply` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Ideal.Quotient.isDomain` `module_finite_of_liesOver` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.trace_eq_zero_of_not_isSeparable` `LinearMap.zero_apply` `zero_add` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Localization.isLocalization` `Function.Involutive.injective` `inv_involutive` `FractionalIdeal.coeIdeal_mul` `inv_div` `mul_div_assoc` `div_self` `mul_one` `inv_inv` `RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `FractionRing.instIsScalarTower` `OreLocalization.instIsScalarTower` `differentialIdeal_le_iff` `instFiniteDimensionalFractionRingOfFinite` `IsIntegralClosure.of_isIntegrallyClosed` `Algebra.IsIntegral.of_finite` `Submodule.map_le_iff_le_comap` `Submodule.mem_comap` `LinearMap.coe_restrictScalars` `FractionalIdeal.coe_one` `FractionalIdeal.mem_coe` `FractionalIdeal.mem_div_iff_of_ne_zero` `FractionalIdeal.mem_coeIdeal` `Submodule.restrictScalars_mem` `Ideal.mem_map_of_mem` `Algebra.algebraMap_intTrace` `smul_eq_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Algebra.smul_def` `IsScalarTower.algebraMap_apply`
`isIntegral_discr_mul_of_mem_traceDual` 📖	mathematical	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `Module.Basis.instFunLike` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.traceDual`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Algebra.toSMul` `Algebra.discr`	—	`Algebra.discr_isUnit_of_basis` `Matrix.mulVec_cramer` `Matrix.mulVec_injective_iff_isUnit` `Matrix.isUnit_iff_isUnit_det` `RingHomInvPair.ids` `Finite.of_fintype` `LinearEquiv.symm_apply_apply` `Module.Basis.equivFun_symm_apply` `IsIntegral.sum` `smul_mul_assoc` `IsScalarTower.right` `LinearEquiv.map_smul` `Algebra.discr_def` `mul_comm` `Algebra.traceMatrix_of_basis_mulVec` `Matrix.mulVec_smul` `Algebra.to_smulCommClass` `Algebra.smul_def` `RingHom.IsIntegralElem.mul` `IsIntegral.algebraMap` `Matrix.cramer_apply` `IsIntegral.det` `Matrix.updateCol_apply` `Algebra.isIntegral_trace` `mul_assoc` `Submodule.mem_traceDual_iff_isIntegral` `IsIntegralClosure.isIntegral_iff` `Submodule.smul_mem`
`map_equiv_traceDual` 📖	mathematical	—	`Submodule.map` `FractionRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `OreLocalization.instSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `OreLocalization.instAlgebra` `Algebra.id` `RingHom.id` `RingHomSurjective.ids` `AlgEquiv.toLinearMap` `FractionRing.algEquiv` `Submodule.traceDual` `FractionRing.field` `FractionRing.liftAlgebra` `FractionRing.instFaithfulSMul` `FractionRing.instIsScalarTower` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IsScalarTower.right` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `IsScalarTower.left` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`IsScalarTower.right` `RingHomSurjective.ids` `FractionRing.instFaithfulSMul` `FractionRing.instIsScalarTower` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `RingHomInvPair.ids` `RingHomSurjective.invPair` `Submodule.map_equiv_eq_comap_symm` `Submodule.ext` `Equiv.forall_congr` `AlgEquiv.symm_apply_apply` `Algebra.trace_eq_of_equiv_equiv` `RingHom.ext` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `IsFractionRing.algEquiv_commutes` `Localization.isLocalization` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `AlgEquiv.apply_symm_apply`
`not_dvd_differentIdeal_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `differentIdeal` `Algebra.IsUnramifiedAt`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsScalarTower.right` `eq_or_ne` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Submonoid.ext` `IsDomain.to_noZeroDivisors` `Ideal.one_notMem` `Localization.isLocalization` `Algebra.FormallyUnramified.iff_of_equiv` `OreLocalization.instIsScalarTower` `Algebra.FormallyUnramified.iff_isSeparable` `Algebra.EssFiniteType.of_finiteType` `Module.Finite.finiteType` `instFiniteDimensionalFractionRingOfFinite` `Algebra.FormallyUnramified.comp` `FractionRing.instIsScalarTower` `IsScalarTower.left` `Algebra.FormallyUnramified.instLocalization` `Algebra.FormallyUnramified.inst` `Ideal.eq_bot_of_comap_eq_bot` `Algebra.IsIntegral.of_finite` `Iff.not` `Ideal.map_eq_bot_iff_of_injective` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Ideal.IsPrime.isMaximal` `IsDedekindDomainDvr.ring_dimensionLEOne` `Ideal.IsPrime.under` `Ideal.over_under` `instIsLocalHomAtPrimeRingHomAlgebraMap` `Localization.AtPrime.isLocalRing` `Algebra.isUnramifiedAt_iff_map_eq` `Mathlib.Tactic.Contrapose.contrapose₂` `dvd_differentIdeal_of_not_isSeparable` `Ideal.IsMaximal.under` `instIsSeparableResidueFieldOfQuotientIdeal` `Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff` `Ideal.map_comap_le` `Ideal.ramificationIdx_spec` `pow_one` `Mathlib.Tactic.Contrapose.contrapose₄` `pow_sub_one_dvd_differentIdeal` `Ideal.uniqueFactorizationMonoid` `Ideal.eq_prime_pow_mul_coprime` `not_dvd_differentIdeal_of_isCoprime_of_isSeparable` `Ideal.isCoprime_iff_sup_eq` `Ideal.ramificationIdx_eq_one_of_isUnramifiedAt` `IsDedekindDomainDvr.toIsNoetherian` `Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count` `instIsSeparableQuotientIdealOfResidueField`
`not_dvd_differentIdeal_of_intTrace_not_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `LinearMap.instFunLike` `Algebra.intTrace` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `IsDedekindDomain.toIsDomain`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `differentIdeal`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsScalarTower.right` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Ideal.map_bot` `RingHom.instRingHomClass` `IsDomain.to_noZeroDivisors` `Ideal.zero_eq_bot` `zero_dvd_iff` `differentIdeal_ne_bot` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `IsIntegralClosure.isLocalization` `Localization.isLocalization` `FractionRing.instIsScalarTower` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `IsIntegralClosure.of_isIntegrallyClosed` `Algebra.IsIntegral.of_finite` `Algebra.IsSeparable.isAlgebraic` `FractionRing.instNontrivial` `Module.Finite.of_isLocalization` `Ideal.dvd_iff_le` `LE.le.trans_eq` `mul_le_mul_left` `Submodule.instMulRightMono` `FractionalIdeal.coeIdeal_le_coeIdeal'` `le_rfl` `mul_le_mul_right` `FractionalIdeal.instMulLeftMono` `coeIdeal_differentIdeal` `FractionalIdeal.coeIdeal_mul` `FractionalIdeal.mul_induction_on` `mul_inv_cancel_left₀` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors` `Submodule.span_induction` `FractionalIdeal.mem_dual` `RingHom.map_one` `Ideal.mul_mem_left` `Algebra.linearMap_apply` `mul_comm` `IsScalarTower.algebraMap_apply` `Algebra.smul_def` `LinearMap.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `mul_one` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MulZeroClass.mul_zero` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `map_add` `SemilinearMapClass.toAddHomClass` `mul_add` `Distrib.leftDistribClass` `Submodule.add_mem` `mul_left_comm` `mul_assoc` `Submodule.smul_mem` `IsLocalization.injective` `Algebra.algebraMap_intTrace`
`not_dvd_differentIdeal_of_isCoprime` 📖	mathematical	`IsCoprime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `differentIdeal`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsScalarTower.right` `Ideal.IsMaximal.eq_of_le` `Ideal.IsMaximal.ne_top` `Ideal.map_le_iff_le_comap` `Ideal.mul_le_right` `Ideal.instIsTwoSided_1` `not_dvd_differentIdeal_of_isCoprime_of_isSeparable` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `module_finite_of_liesOver` `PerfectField.ofFinite`
`not_dvd_differentIdeal_of_isCoprime_of_isSeparable` 📖	mathematical	`IsCoprime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `differentIdeal`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsScalarTower.right` `Ideal.instIsTwoSided_1` `RingHom.instRingHomClass` `Ideal.map_le_iff_le_comap` `Ideal.mul_le_left` `IsScalarTower.of_algebraMap_eq'` `Module.Finite.of_restrictScalars_finite` `Module.Finite.quotient` `Algebra.trace_ne_zero` `module_finite_of_liesOver` `RingEquiv.map_mul'` `RingEquiv.map_add'` `Ideal.Quotient.mk_surjective` `not_dvd_differentIdeal_of_intTrace_not_mem` `Ideal.quotientMulEquivQuotientProd_snd` `AlgEquiv.apply_symm_apply` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Ideal.Quotient.eq_zero_iff_mem` `Algebra.trace_quotient_eq_of_isDedekindDomain` `Algebra.trace_eq_of_algEquiv` `Algebra.trace_prod_apply` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Ideal.Quotient.isDomain` `Ideal.IsMaximal.isPrime'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_zero`
`pow_sub_one_dvd_differentIdeal` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.instPowNat` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`differentIdeal`	—	`IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsScalarTower.right` `IsIntegralClosure.isLocalization` `Localization.isLocalization` `FractionRing.instIsScalarTower` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `IsIntegralClosure.of_isIntegrallyClosed` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Algebra.IsIntegral.of_finite` `Algebra.IsSeparable.isAlgebraic` `FractionRing.instNontrivial` `IsDomain.to_noZeroDivisors` `Module.Finite.of_isLocalization` `pow_zero` `one_dvd` `pow_sub_one_dvd_differentIdeal_aux`
`pow_sub_one_dvd_differentIdeal_aux` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Submodule.instPowNat` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`differentIdeal`	—	`IsScalarTower.right` `Dvd.dvd.trans` `pow_dvd_pow` `Iff.not` `Ideal.map_eq_bot_iff_of_injective` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Submodule.mul_bot` `Ideal.zero_eq_bot` `zero_dvd_iff` `zero_pow` `mul_comm` `pow_one` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Ideal.isCancelMulZero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `Ideal.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `mul_assoc` `mul_pow` `pow_add` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq_zero_iff_mem` `Algebra.trace_quotient_eq_of_isDedekindDomain` `isNilpotent_iff_eq_zero` `Ideal.Quotient.noZeroDivisors` `Ideal.IsMaximal.isPrime'` `Algebra.isNilpotent_trace_of_isNilpotent` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.dvd_iff_le` `Ideal.pow_mem_pow` `Function.Involutive.injective` `inv_involutive` `inv_inv` `FractionalIdeal.coeIdeal_mul` `inv_div` `mul_div_assoc` `div_self` `mul_one` `RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul` `differentialIdeal_le_iff` `Submodule.map_le_iff_le_comap` `Submodule.mem_comap` `LinearMap.coe_restrictScalars` `FractionalIdeal.coe_one` `FractionalIdeal.mem_coe` `FractionalIdeal.mem_div_iff_of_ne_zero` `FractionalIdeal.mem_coeIdeal` `Submodule.restrictScalars_mem` `Ideal.mem_map_of_mem` `Algebra.algebraMap_intTrace` `smul_eq_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Algebra.smul_def` `IsScalarTower.algebraMap_apply`
`traceForm_dualSubmodule_adjoin` 📖	mathematical	`Algebra.adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Set` `Set.instSingletonSet` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing`	`LinearMap.BilinForm.dualSubmodule` `Ring.toAddCommGroup` `Algebra.toModule` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toSemiring` `Algebra.traceForm` `DFunLike.coe` `OrderEmbedding` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `LinearMap` `RingHom.id` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.derivative` `minpoly`	—	`Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsDomain` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `IsPrincipalIdealRing.isDedekindDomain` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SetLike.mem_coe` `Algebra.subset_adjoin` `Set.mem_singleton` `Algebra.adjoin.powerBasis'_gen` `traceForm_nondegenerate` `Finite.of_fintype` `Module.Basis.traceDual_powerBasis_eq` `Submodule.span_range_natDegree_eq_adjoin` `minpoly.monic` `minpoly.aeval` `Set.ext` `minpoly.isIntegrallyClosed_eq_field_fractions'` `Polynomial.Monic.natDegree_map` `Finset.coe_image` `Finset.coe_range` `PowerBasis.basis_eq_pow` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `span_coeff_minpolyDiv` `LinearMap.BilinForm.dualSubmodule_span_of_basis` `Submodule.smul_span` `div_eq_inv_mul` `Set.image_congr` `minpolyDiv_eq_of_isIntegrallyClosed` `le_antisymm` `Submodule.span_le` `Submodule.subset_span` `Polynomial.coeff_eq_zero_of_natDegree_lt` `natDegree_minpolyDiv_succ` `PowerBasis.natDegree_minpoly` `MulZeroClass.mul_zero` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`

---

← Back to Index