Documentation Verification Report

LinearDisjoint

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

Statistics

Metric	Count
Definitions `ofIsCoprimeDifferentIdeal`	1
Theorems `adjoin_union_eq_top_of_isCoprime_differentialIdeal`, `differentIdeal_dvd_map_differentIdeal`, `differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime`, `differentIdeal_eq_map_differentIdeal`, `map_differentIdeal_dvd_differentIdeal`, `range_sup_range_eq_top_of_isCoprime_differentIdeal`, `ofIsCoprimeDifferentIdeal_apply`, `traceDual_eq_span_map_traceDual_of_linearDisjoint`, `traceDual_le_span_map_traceDual`	9
Total	10

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_union_eq_top_of_isCoprime_differentialIdeal` 📖	mathematical	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `Subalgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `IntermediateField.toSubalgebra` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsCoprime` `Ideal` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `differentIdeal` `Algebra.adjoin`	`Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Set` `Set.instUnion` `Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IntermediateField.isScalarTower_mid'` `Algebra.adjoin_union` `IsScalarTower.coe_toAlgHom'` `AlgHom.map_adjoin` `Algebra.map_top` `range_sup_range_eq_top_of_isCoprime_differentIdeal`
`differentIdeal_dvd_map_differentIdeal` 📖	mathematical	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `differentIdeal` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Module.IsReflexive.to_isTorsionFree` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.isScalarTower_mid'` `toIsDomain` `FractionRing.instFaithfulSMul` `Module.Free.instFaithfulSMulOfNontrivial` `IsDomain.toNontrivial` `Algebra.IsSeparable.of_equiv_equiv` `RingHom.ext` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `IsFractionRing.algEquiv_commutes` `IntermediateField.isScalarTower` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `Module.IsReflexive.to_isTorsionFree` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `Ideal.dvd_iff_le` `FractionalIdeal.coeIdeal_le_coeIdeal` `IsDedekindDomainDvr.isIntegrallyClosed` `isDedekindDomainDvr` `IntermediateField.finiteDimensional_right` `IsDomain.to_noZeroDivisors` `coeIdeal_differentIdeal` `FractionalIdeal.extendedHomₐ_coeIdeal_eq_map` `FractionalIdeal.le_inv_comm` `map_ne_zero` `FractionalIdeal.instNontrivialNonZeroDivisors` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Iff.not` `FractionalIdeal.coeIdeal_eq_zero` `differentIdeal_ne_bot` `NeZero.one` `map_inv₀` `IntermediateField.finiteDimensional_left` `IsIntegralClosure.of_isIntegrallyClosed` `Algebra.IsIntegral.of_finite` `inv_inv` `FractionalIdeal.coe_le_coe` `FractionalIdeal.coe_dual_one` `FractionalIdeal.coe_extendedHomₐ_eq_span` `FractionalIdeal.coeToSet_coeToSubmodule` `Submodule.span_mono` `Submodule.traceDual_le_span_map_traceDual` `Submodule.span_eq` `Submodule.span_span_of_tower` `Submodule.span_coe_eq_restrictScalars`
`differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime` 📖	mathematical	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsCoprime` `Ideal` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `differentIdeal`	`differentIdeal` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `toIsDomain`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IntermediateField.isScalarTower_mid'` `IsScalarTower.right` `differentIdeal_eq_differentIdeal_mul_differentIdeal` `mul_comm` `differentIdeal_eq_map_differentIdeal`
`differentIdeal_eq_map_differentIdeal` 📖	mathematical	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsCoprime` `Ideal` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `differentIdeal`	`differentIdeal` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IntermediateField.isScalarTower_mid'` `dvd_antisymm` `Ideal.isCancelMulZero` `Unique.instSubsingleton` `differentIdeal_dvd_map_differentIdeal` `Algebra.IsIntegral.of_finite` `Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors` `Module.Free.instFaithfulSMulOfNontrivial` `Algebra.IsAlgebraic.of_finite` `IsDomain.to_noZeroDivisors` `map_differentIdeal_dvd_differentIdeal`
`map_differentIdeal_dvd_differentIdeal` 📖	mathematical	`IsCoprime` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `differentIdeal`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Submodule.instNonUnitalSemiring` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `differentIdeal`	—	`toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsScalarTower.right` `differentIdeal_eq_differentIdeal_mul_differentIdeal` `IsCoprime.dvd_of_dvd_mul_right` `IsCoprime.symm` `dvd_of_mul_left_eq`
`range_sup_range_eq_top_of_isCoprime_differentIdeal` 📖	mathematical	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `Subalgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `IntermediateField.toSubalgebra` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsCoprime` `Ideal` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `differentIdeal`	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `AlgHom.range` `IsScalarTower.toAlgHom` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IntermediateField.isScalarTower_mid'` `Algebra.eq_top_iff` `RingHomInvPair.ids` `Module.Basis.sum_repr` `Subalgebra.sum_mem` `Algebra.smul_def` `Subalgebra.mul_mem` `Algebra.mem_sup_left` `Algebra.mem_sup_right` `Module.Basis.ofIsCoprimeDifferentIdeal_apply`

Module.Basis

Definitions

Name	Category	Theorems
`ofIsCoprimeDifferentIdeal` 📖	CompOp	1 math math: `ofIsCoprimeDifferentIdeal_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofIsCoprimeDifferentIdeal_apply` 📖	mathematical	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `Subalgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `IntermediateField.toSubalgebra` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsCoprime` `Ideal` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `differentIdeal`	`DFunLike.coe` `Module.Basis` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `instFunLike` `ofIsCoprimeDifferentIdeal` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IntermediateField.isScalarTower_mid'`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`traceDual_eq_span_map_traceDual_of_linearDisjoint` 📖	mathematical	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsCoprime` `Ideal` `CommRing.toCommSemiring` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `differentIdeal`	`span` `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` `Set.image` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `SubfieldClass.toSubringClass` `Field.toDivisionRing` `IntermediateField.instSubfieldClass` `RingHom.instFunLike` `algebraMap` `IntermediateField.instAlgebraSubtypeMem` `Algebra.id` `SetLike.coe` `Submodule` `IntermediateField.toField` `setLike` `traceDual` `IntermediateField.algebra'` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IntermediateField.isScalarTower` `one` `restrictScalars`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsDedekindDomain.toIsDomain` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IntermediateField.isScalarTower_mid'` `Module.Free.instFaithfulSMulOfNontrivial` `Algebra.IsSeparable.of_equiv_equiv` `RingHom.ext` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `IsFractionRing.algEquiv_commutes` `IntermediateField.isScalarTower` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `dvd_of_eq` `IsDedekindDomain.differentIdeal_eq_map_differentIdeal` `IntermediateField.finiteDimensional_left` `IsIntegralClosure.of_isIntegrallyClosed` `IsDedekindDomainDvr.isIntegrallyClosed` `IsDedekindDomain.isDedekindDomainDvr` `Algebra.IsIntegral.of_finite` `IsDomain.to_noZeroDivisors` `FractionalIdeal.coe_dual_one` `FractionalIdeal.coeToSet_coeToSubmodule` `IntermediateField.finiteDimensional_right` `FractionalIdeal.coe_extendedHomₐ_eq_span` `FractionalIdeal.coe_le_coe` `inv_inv` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coeIdeal_differentIdeal` `FractionalIdeal.extendedHomₐ_coeIdeal_eq_map` `FractionalIdeal.inv_le_comm` `NeZero.one` `FractionalIdeal.instNontrivialNonZeroDivisors` `FractionalIdeal.extendedHomₐ_eq_zero_iff` `FractionalIdeal.coeIdeal_eq_zero` `differentIdeal_ne_bot` `FractionalIdeal.coeIdeal_le_coeIdeal` `Ideal.dvd_iff_le` `le_antisymm` `SetLike.coe_subset_coe` `instIsConcreteLE` `subset_trans` `Set.instIsTransSubset` `span_span_of_tower` `subset_span` `traceDual_le_span_map_traceDual`
`traceDual_le_span_map_traceDual` 📖	mathematical	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`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` `restrictScalars` `Algebra.toSMul` `traceDual` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `Algebra.id` `Semifield.toCommSemiring` `one` `span` `Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `SubfieldClass.toSubringClass` `Field.toDivisionRing` `IntermediateField.instSubfieldClass` `RingHom.instFunLike` `algebraMap` `SetLike.coe` `setLike` `IntermediateField.algebra'` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IntermediateField.isScalarTower`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.isScalarTower_mid'` `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` `IntermediateField.isAlgebraic_tower_bot` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.isScalarTower` `IntermediateField.finiteDimensional_right` `Finite.of_fintype` `RingHomInvPair.ids` `Module.Basis.mem_span_iff_repr_mem` `SubsemiringClass.nontrivial` `Module.Basis.traceDual_repr_apply` `mem_traceDual` `IntermediateField.LinearDisjoint.basisOfBasisRight_apply` `Module.Basis.localizationLocalization_apply` `IsScalarTower.algebraMap_apply` `mem_one` `IntermediateField.finiteDimensional_left` `Module.Basis.traceDual_eq_iff` `Algebra.traceForm_apply` `IsScalarTower.coe_toAlgHom'` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IntermediateField.LinearDisjoint.trace_algebraMap` `Module.Basis.trace_traceDual_mul` `MonoidWithZeroHom.map_ite_one_zero` `RingHomClass.toMonoidWithZeroHomClass` `RingHomSurjective.ids` `traceDual_span_of_basis` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Module.Basis.localizationLocalization_span` `ext` `map_span` `AlgHom.coe_toLinearMap` `Set.range_comp` `span_span_of_tower`

---

← Back to Index