LinearDisjoint

📁 Source: Mathlib/FieldTheory/LinearDisjoint.lean

Statistics

Metric	Count
Definitions `basisOfBasisLeft`, `basisOfBasisRight`	2
Theorems `isField_of_isAlgebraic`, `adjoin_rank_eq_rank_left_of_isAlgebraic`, `adjoin_rank_eq_rank_left_of_isAlgebraic_left`, `adjoin_rank_eq_rank_left_of_isAlgebraic_right`, `adjoin_rank_eq_rank_right_of_isAlgebraic`, `adjoin_rank_eq_rank_right_of_isAlgebraic_left`, `adjoin_rank_eq_rank_right_of_isAlgebraic_right`, `algEquiv_of_isAlgebraic`, `algebraMap_basisOfBasisRight_repr_apply`, `basisOfBasisLeft_apply`, `basisOfBasisLeft_repr_apply`, `basisOfBasisRight_apply`, `bot_left`, `bot_right`, `eq_bot_of_self`, `exists_field_of_isDomain`, `finrank_left_eq_finrank`, `finrank_right_eq_finrank`, `finrank_sup`, `iff_inf_eq_bot`, `inf_eq_bot`, `isDomain`, `isDomain'`, `isField_of_forall`, `isField_of_isAlgebraic`, `isField_of_isAlgebraic'`, `lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic`, `lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left`, `lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right`, `lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic`, `lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left`, `lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right`, `linearIndependent_left`, `linearIndependent_mul`, `linearIndependent_mul'`, `linearIndependent_right`, `linearIndependent_right'`, `map`, `map'`, `map''`, `norm_algebraMap`, `of_basis_left`, `of_basis_mul`, `of_basis_mul'`, `of_basis_right`, `of_basis_right'`, `of_finrank_coprime`, `of_finrank_sup`, `of_inf_eq_bot`, `of_isField`, `of_isField'`, `of_le`, `of_le'`, `of_le_left`, `of_le_right`, `of_le_right'`, `rank_right_mul_adjoin_rank_eq_of_isAlgebraic`, `rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left`, `rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right`, `rank_sup`, `self_right`, `symm'`, `trace_algebraMap`, `linearDisjoint_comm`, `linearDisjoint_comm'`, `linearDisjoint_iff`, `linearDisjoint_iff'`	67
Total	69

Algebra.TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isField_of_isAlgebraic` 📖	mathematical	`Algebra.IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`IsField` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemiring`	—	`Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `RingHom.injective` `DivisionRing.isSimpleRing` `IsScalarTower.left` `IsScalarTower.to_smulCommClass` `Subalgebra.instIsScalarTowerSubtypeMem` `IntermediateField.sup_toSubalgebra_of_isAlgebraic` `AlgEquiv.isAlgebraic_iff` `MulEquiv.isField` `Field.toIsField`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearDisjoint_comm` 📖	mathematical	—	`LinearDisjoint` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `instAlgebraSubtypeMem` `isScalarTower_mid'`	—	`IsScalarTower.left` `isScalarTower_mid'` `LinearDisjoint.symm`
`linearDisjoint_comm'` 📖	mathematical	—	`LinearDisjoint` `AlgHom.fieldRange` `IsScalarTower.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`LinearDisjoint.symm'`
`linearDisjoint_iff` 📖	mathematical	—	`LinearDisjoint` `Subalgebra.LinearDisjoint` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSubalgebra` `AlgHom.range` `CommSemiring.toSemiring` `IsScalarTower.toAlgHom`	—	—
`linearDisjoint_iff'` 📖	mathematical	—	`LinearDisjoint` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `instAlgebraSubtypeMem` `isScalarTower_mid'` `Subalgebra.LinearDisjoint` `toSubalgebra`	—	`IsScalarTower.left` `isScalarTower_mid'` `linearDisjoint_iff` `Subalgebra.ext`

IntermediateField.LinearDisjoint

Definitions

Name	Category	Theorems
`basisOfBasisLeft` 📖	CompOp	2 math math: `basisOfBasisLeft_apply`, `basisOfBasisLeft_repr_apply`
`basisOfBasisRight` 📖	CompOp	2 math math: `algebraMap_basisOfBasisRight_repr_apply`, `basisOfBasisRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_rank_eq_rank_left_of_isAlgebraic` 📖	mathematical	`IntermediateField.LinearDisjoint` `Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`Module.rank` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.module'`	—	`IsScalarTower.left` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic` `Algebra.adjoin_toSubsemiring` `Set.ext` `rank_eq_of_equiv_equiv` `AlgEquiv.bijective` `Algebra.smul_def` `Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left` `Module.Free.of_divisionRing` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass`
`adjoin_rank_eq_rank_left_of_isAlgebraic_left` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Module.rank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `SetLike.coe` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.left` `adjoin_rank_eq_rank_left_of_isAlgebraic`
`adjoin_rank_eq_rank_left_of_isAlgebraic_right` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Module.rank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `SetLike.coe` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`adjoin_rank_eq_rank_left_of_isAlgebraic` `IsScalarTower.left`
`adjoin_rank_eq_rank_right_of_isAlgebraic` 📖	mathematical	`IntermediateField.LinearDisjoint` `Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`Module.rank` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.extendScalars` `IntermediateField.restrictScalars` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.instModuleSubtypeMem_1`	—	`IsScalarTower.left` `IntermediateField.subset_adjoin` `Cardinal.lift_id` `lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic`
`adjoin_rank_eq_rank_right_of_isAlgebraic_left` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Module.rank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring` `IntermediateField.extendScalars` `IntermediateField.restrictScalars` `IntermediateField.adjoin` `SetLike.coe` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.instModuleSubtypeMem_1` `Algebra.toModule`	—	`IsScalarTower.left` `adjoin_rank_eq_rank_right_of_isAlgebraic`
`adjoin_rank_eq_rank_right_of_isAlgebraic_right` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Module.rank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring` `IntermediateField.extendScalars` `IntermediateField.restrictScalars` `IntermediateField.adjoin` `SetLike.coe` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.instModuleSubtypeMem_1` `Algebra.toModule`	—	`adjoin_rank_eq_rank_right_of_isAlgebraic` `IsScalarTower.left`
`algEquiv_of_isAlgebraic` 📖	—	`IntermediateField.LinearDisjoint` `Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	—	—	`IsScalarTower.left` `of_isField` `MulEquiv.isField` `isField_of_isAlgebraic` `IsScalarTower.to_smulCommClass` `IntermediateField.isScalarTower`
`algebraMap_basisOfBasisRight_repr_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`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `RingHom.instFunLike` `algebraMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule` `Finsupp.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `basisOfBasisRight` `IntermediateField.module'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply` `IntermediateField.linearDisjoint_iff'`
`basisOfBasisLeft_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`	`DFunLike.coe` `Module.Basis` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule` `Module.Basis.instFunLike` `basisOfBasisLeft` `RingHom` `Semiring.toNonAssocSemiring` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `RingHom.instFunLike` `algebraMap` `IntermediateField.module'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.basisOfBasisLeft_apply` `IntermediateField.linearDisjoint_iff'`
`basisOfBasisLeft_repr_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`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `RingHom.instFunLike` `algebraMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule` `Finsupp.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `basisOfBasisLeft` `IntermediateField.module'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply` `IntermediateField.linearDisjoint_iff'`
`basisOfBasisRight_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`	`DFunLike.coe` `Module.Basis` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule` `Module.Basis.instFunLike` `basisOfBasisRight` `RingHom` `Semiring.toNonAssocSemiring` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `RingHom.instFunLike` `algebraMap` `IntermediateField.module'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_apply` `IntermediateField.linearDisjoint_iff'`
`bot_left` 📖	mathematical	—	`IntermediateField.LinearDisjoint` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Subalgebra.LinearDisjoint.bot_left`
`bot_right` 📖	mathematical	—	`IntermediateField.LinearDisjoint` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `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'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.linearDisjoint_iff'` `Subalgebra.LinearDisjoint.bot_right`
`eq_bot_of_self` 📖	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'`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `inf_eq_bot` `inf_idem`
`exists_field_of_isDomain` 📖	mathematical	—	`IntermediateField.LinearDisjoint` `AlgHom.fieldRange` `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'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `RingHom.injective` `DivisionRing.isSimpleRing` `IntermediateField.linearDisjoint_iff'`
`finrank_left_eq_finrank` 📖	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`	`Module.finrank` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule` `IntermediateField.module'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `finrank_sup` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Module.finrank_mul_finrank` `Module.Free.of_divisionRing` `IntermediateField.finrank_top'`
`finrank_right_eq_finrank` 📖	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`	`Module.finrank` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule` `IntermediateField.module'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `finrank_left_eq_finrank` `symm` `sup_comm`
`finrank_sup` 📖	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'`	`Module.finrank` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `IntermediateField.module'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `rank_sup`
`iff_inf_eq_bot` 📖	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'` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `inf_eq_bot` `of_inf_eq_bot`
`inf_eq_bot` 📖	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'`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.toSubalgebra_injective` `Subalgebra.LinearDisjoint.inf_eq_bot` `IntermediateField.linearDisjoint_iff'`
`isDomain` 📖	mathematical	`IntermediateField.LinearDisjoint`	`IsDomain` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.module'` `CommSemiring.toSemiring` `Algebra.toSMul` `Algebra.id` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.TensorProduct.instSemiring` `IntermediateField.algebra'`	—	`IsScalarTower.left` `Subalgebra.LinearDisjoint.isDomain` `instIsDomain` `MulEquiv.isDomain` `IsScalarTower.to_smulCommClass` `IntermediateField.isScalarTower` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`isDomain'` 📖	mathematical	`IntermediateField.LinearDisjoint` `AlgHom.fieldRange` `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'`	`IsDomain` `TensorProduct` `Algebra.TensorProduct.instSemiring`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.isDomain_of_injective` `instIsDomain` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`isField_of_forall` 📖	mathematical	`IntermediateField.LinearDisjoint` `AlgHom.fieldRange` `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'`	`IsField` `TensorProduct` `Algebra.TensorProduct.instSemiring`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Ideal.exists_maximal` `Module.FaithfullyFlat.lTensor_nontrivial` `Module.FaithfullyFlat.instOfNontrivialOfFree` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `not_imp_not` `Ring.ne_bot_of_isMaximal_of_not_isField` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `IsScalarTower.to_smulCommClass` `Subalgebra.instIsScalarTowerSubtypeMem` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `RingHom.injective` `DivisionRing.isSimpleRing` `Algebra.TensorProduct.ext` `TensorProduct.isScalarTower` `AlgHom.ext` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `mul_one` `TensorProduct.isScalarTower_left` `one_mul` `Ideal.instIsTwoSided_1` `RingHom.instRingHomClass` `Ideal.mk_ker` `RingHom.injective_iff_ker_eq_bot`
`isField_of_isAlgebraic` 📖	mathematical	`IntermediateField.LinearDisjoint` `Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`IsField` `TensorProduct` `IntermediateField.module'` `Algebra.TensorProduct.instSemiring`	—	`IsScalarTower.left` `isDomain` `Algebra.TensorProduct.isField_of_isAlgebraic`
`isField_of_isAlgebraic'` 📖	mathematical	`IntermediateField.LinearDisjoint` `AlgHom.fieldRange` `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'` `Algebra.IsAlgebraic` `DivisionRing.toRing` `Field.toDivisionRing`	`IsField` `TensorProduct` `Algebra.TensorProduct.instSemiring`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `isDomain'` `Algebra.TensorProduct.isField_of_isAlgebraic`
`lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic` 📖	mathematical	`IntermediateField.LinearDisjoint` `Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`Cardinal.lift` `Module.rank` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.extendScalars` `IntermediateField.restrictScalars` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.instModuleSubtypeMem_1`	—	`IsScalarTower.left` `IntermediateField.subset_adjoin` `LinearEquiv.lift_rank_eq` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_right` `Module.Free.of_divisionRing` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic` `Algebra.adjoin_toSubsemiring` `Set.union_comm` `Set.ext` `rank_eq_of_equiv_equiv` `Function.bijective_id` `Algebra.smul_def`
`lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Cardinal.lift` `Module.rank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring` `IntermediateField.extendScalars` `IntermediateField.restrictScalars` `IntermediateField.adjoin` `SetLike.coe` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.instModuleSubtypeMem_1` `Algebra.toModule`	—	`IsScalarTower.left` `lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic`
`lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Cardinal.lift` `Module.rank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring` `IntermediateField.extendScalars` `IntermediateField.restrictScalars` `IntermediateField.adjoin` `SetLike.coe` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.instModuleSubtypeMem_1` `Algebra.toModule`	—	`lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic` `IsScalarTower.left`
`lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic` 📖	mathematical	`IntermediateField.LinearDisjoint` `Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`Cardinal` `Cardinal.instMul` `Cardinal.lift` `Module.rank` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`IsScalarTower.left` `IntermediateField.subset_adjoin` `lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic` `Cardinal.lift_mul` `rank_mul_rank` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `IntermediateField.isScalarTower_mid'`
`lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Cardinal` `Cardinal.instMul` `Cardinal.lift` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.toField` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`IsScalarTower.left` `lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic`
`lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Cardinal` `Cardinal.instMul` `Cardinal.lift` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.toField` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic` `IsScalarTower.left`
`linearIndependent_left` 📖	mathematical	`IntermediateField.LinearDisjoint` `LinearIndependent` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`DFunLike.coe` `AlgHom` `IntermediateField.algebra'` `Field.toCommRing` `AlgHom.funLike` `IntermediateField.val`	—	`IsScalarTower.left` `LinearIndependent.map_of_injective_injective` `Subalgebra.LinearDisjoint.linearIndependent_left_of_flat` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `EquivLike.toEmbeddingLike` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Algebra.smul_def`
`linearIndependent_mul` 📖	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'` `LinearIndependent` `IntermediateField.module'`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left` `IntermediateField.linearDisjoint_iff'` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing`
`linearIndependent_mul'` 📖	mathematical	`IntermediateField.LinearDisjoint` `LinearIndependent` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.left` `Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `RingHomInvPair.ids` `LinearIndependent.map'` `LinearEquiv.ker`
`linearIndependent_right` 📖	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'` `LinearIndependent` `IntermediateField.module'`	`DFunLike.coe` `AlgHom` `Field.toCommRing` `AlgHom.funLike` `IntermediateField.val` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.linearIndependent_right_of_flat` `IntermediateField.linearDisjoint_iff'` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing`
`linearIndependent_right'` 📖	mathematical	`IntermediateField.LinearDisjoint` `LinearIndependent` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `IntermediateField.toField` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`Subalgebra.LinearDisjoint.linearIndependent_right_of_flat` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `RingHomInvPair.ids` `LinearIndependent.map'` `LinearEquiv.ker`
`map` 📖	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'`	`IntermediateField.map`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.linearDisjoint_iff'` `Subalgebra.LinearDisjoint.map` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`map'` 📖	mathematical	`IntermediateField.LinearDisjoint`	`IntermediateField.map` `IsScalarTower.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IntermediateField.linearDisjoint_iff` `Subalgebra.LinearDisjoint.map` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `AlgHom.ext` `IsScalarTower.algebraMap_apply` `AlgHom.range_comp`
`map''` 📖	—	`IntermediateField.LinearDisjoint` `AlgHom.fieldRange` `IsScalarTower.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	—	`IntermediateField.linearDisjoint_iff` `Subalgebra.LinearDisjoint.map` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `AlgHom.fieldRange_toSubalgebra` `AlgHom.ext` `IsScalarTower.algebraMap_apply`
`norm_algebraMap` 📖	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`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `Algebra.norm` `RingHom` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.norm_algebraMap` `IntermediateField.linearDisjoint_iff'` `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` `IntermediateField.isAlgebraic_tower_bot` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `FiniteDimensional.finiteDimensional_subalgebra`
`of_basis_left` 📖	mathematical	`LinearIndependent` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.toField` `IntermediateField.algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgHom.funLike` `IntermediateField.val` `Module.Basis` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.module'` `Module.Basis.instFunLike`	`IntermediateField.LinearDisjoint`	—	`IsScalarTower.left` `Subalgebra.LinearDisjoint.of_basis_left` `LinearIndependent.map_of_surjective_injective` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `AlgEquiv.surjective` `Algebra.smul_def`
`of_basis_mul` 📖	mathematical	`LinearIndependent` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Module.Basis.instFunLike`	`IntermediateField.LinearDisjoint` `IntermediateField.algebra'` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.linearDisjoint_iff'` `Subalgebra.LinearDisjoint.of_basis_mul`
`of_basis_mul'` 📖	mathematical	`LinearIndependent` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Module.Basis.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`IntermediateField.LinearDisjoint`	—	`IsScalarTower.left` `Subalgebra.LinearDisjoint.of_basis_mul` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`of_basis_right` 📖	mathematical	`LinearIndependent` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.toField` `IntermediateField.algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgHom.funLike` `IntermediateField.val` `Module.Basis` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.module'` `Module.Basis.instFunLike` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	`IntermediateField.LinearDisjoint` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.linearDisjoint_iff'` `Subalgebra.LinearDisjoint.of_basis_right`
`of_basis_right'` 📖	mathematical	`LinearIndependent` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `Module.Basis` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Module.Basis.instFunLike` `IntermediateField.toField` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	`IntermediateField.LinearDisjoint`	—	`Subalgebra.LinearDisjoint.of_basis_right` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`of_finrank_coprime` 📖	mathematical	`Module.finrank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`IntermediateField.LinearDisjoint`	—	`IsScalarTower.left` `Subalgebra.LinearDisjoint.of_finrank_coprime_of_free` `Module.Free.of_divisionRing` `LinearEquiv.finrank_eq` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`of_finrank_sup` 📖	mathematical	`Module.finrank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`IntermediateField.LinearDisjoint` `IntermediateField.algebra'` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.linearDisjoint_iff'` `Subalgebra.LinearDisjoint.of_finrank_sup_of_free` `Module.Free.of_divisionRing` `IntermediateField.sup_toSubalgebra_of_left`
`of_inf_eq_bot` 📖	mathematical	`IntermediateField` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`IntermediateField.LinearDisjoint` `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'`	—	`IsScalarTower.left` `le_sup_left` `le_sup_right` `IntermediateField.lift_restrict` `IntermediateField.isScalarTower` `IntermediateField.isScalarTower_mid'` `IntermediateField.lift_top` `IntermediateField.lift_sup` `IntermediateField.lift_bot` `IntermediateField.lift_inf` `IsGalois.of_algEquiv` `IntermediateField.finiteDimensional_sup` `map`
`of_isField` 📖	mathematical	`IsField` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.module'` `CommSemiring.toSemiring` `Algebra.toSMul` `Algebra.id` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.TensorProduct.instSemiring` `IntermediateField.algebra'`	`IntermediateField.LinearDisjoint`	—	`IsScalarTower.left` `Subalgebra.LinearDisjoint.of_isField` `MulEquiv.isField` `IsScalarTower.to_smulCommClass` `IntermediateField.isScalarTower` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`of_isField'` 📖	mathematical	`IsField` `TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.TensorProduct.instSemiring`	`IntermediateField.LinearDisjoint` `AlgHom.fieldRange` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.linearDisjoint_iff'` `Subalgebra.LinearDisjoint.of_isField` `MulEquiv.isField` `IsScalarTower.to_smulCommClass` `Subalgebra.instIsScalarTowerSubtypeMem` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`of_le` 📖	—	`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'` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder`	—	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `of_le_right` `of_le_left`
`of_le'` 📖	—	`IntermediateField.LinearDisjoint` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder`	—	—	`of_le_right'` `of_le_left`
`of_le_left` 📖	—	`IntermediateField.LinearDisjoint` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder`	—	—	`Subalgebra.LinearDisjoint.of_le_left_of_flat` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing`
`of_le_right` 📖	—	`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'` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder`	—	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.linearDisjoint_iff'` `Subalgebra.LinearDisjoint.of_le_right_of_flat` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing`
`of_le_right'` 📖	—	`IntermediateField.LinearDisjoint`	—	—	`Subalgebra.LinearDisjoint.of_le_right_of_flat` `AlgHom.ext` `IsScalarTower.algebraMap_apply` `AlgHom.range_comp_le_range` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.instOfNontrivialOfFree` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing`
`rank_right_mul_adjoin_rank_eq_of_isAlgebraic` 📖	mathematical	`IntermediateField.LinearDisjoint` `Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`Cardinal` `Cardinal.instMul` `Module.rank` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`IsScalarTower.left` `Cardinal.lift_id` `lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic`
`rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Cardinal` `Cardinal.instMul` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.toField` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`IsScalarTower.left` `rank_right_mul_adjoin_rank_eq_of_isAlgebraic`
`rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right` 📖	mathematical	`IntermediateField.LinearDisjoint`	`Cardinal` `Cardinal.instMul` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.toField` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`rank_right_mul_adjoin_rank_eq_of_isAlgebraic` `IsScalarTower.left`
`rank_sup` 📖	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'`	`Module.rank` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `IntermediateField.module'` `Cardinal` `Cardinal.instMul`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.le_sup_toSubalgebra` `LE.le.antisymm` `IntermediateField.rank_sup_le` `LE.le.trans` `Eq.ge` `Subalgebra.LinearDisjoint.rank_sup_of_free` `IntermediateField.linearDisjoint_iff'` `Module.Free.of_divisionRing` `LinearMap.rank_le_of_injective` `Subalgebra.inclusion_injective`
`self_right` 📖	mathematical	—	`IntermediateField.LinearDisjoint` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield` `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`	—	`Subalgebra.LinearDisjoint.bot_right`
`symm'` 📖	—	`IntermediateField.LinearDisjoint` `AlgHom.fieldRange` `IsScalarTower.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	—	`Subalgebra.LinearDisjoint.symm`
`trace_algebraMap` 📖	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`	`DFunLike.coe` `LinearMap` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `Algebra.trace` `RingHom` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Subalgebra.LinearDisjoint.trace_algebraMap` `IntermediateField.linearDisjoint_iff'` `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` `IntermediateField.isAlgebraic_tower_bot` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `FiniteDimensional.finiteDimensional_subalgebra`

---

← Back to Index