Operations

📁 Source: Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

Statistics

Metric	Count
Definitions `toTwoSided`, `mapTwoSidedIdeal`, `asIdeal`, `asIdealOpposite`, `comap`, `fromIdeal`, `instSMulMulOppositeSubtypeMem`, `instSMulSubtypeMem`, `leftModule`, `map`, `orderIsoIdeal`, `orderIsoIsTwoSided`, `rightModule`, `span`, `subtype`, `subtypeMop`	16
Theorems `asIdeal_toTwoSided`, `coe_toTwoSided`, `instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided`, `mem_toTwoSided`, `toTwoSided_asIdeal`, `mapTwoSidedIdeal_apply`, `mapTwoSidedIdeal_symm`, `bot_asIdeal`, `coe_asIdeal`, `coe_mop_smul`, `coe_smul`, `coe_subtype`, `comap_comap`, `comap_le_comap`, `gc`, `instIsTwoSidedCoeOrderHomIdealAsIdeal`, `instSMulCommClassMulOppositeSubtypeMem`, `map_mono`, `mem_asIdeal`, `mem_asIdealOpposite`, `mem_comap`, `mem_fromIdeal`, `mem_span_iff`, `mem_span_iff_mem_addSubgroup_closure`, `mem_span_iff_mem_addSubgroup_closure_absorbing`, `mem_span_iff_mem_addSubgroup_closure_nonunital`, `orderIsoIsTwoSided_apply_coe`, `orderIsoIsTwoSided_symm_apply`, `set_mul_subset`, `span_induction`, `span_le`, `span_mono`, `subset_mul_set`, `subset_span`, `subtypeMop_apply`, `subtypeMop_injective`, `subtype_apply`, `subtype_injective`, `top_asIdeal`	39
Total	55

Ideal

Definitions

Name	Category	Theorems
`toTwoSided` 📖	CompOp	4 math math: `mem_toTwoSided`, `toTwoSided_asIdeal`, `coe_toTwoSided`, `asIdeal_toTwoSided`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asIdeal_toTwoSided` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ideal` `Ring.toSemiring` `PartialOrder.toPreorder` `TwoSidedIdeal.instPartialOrder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `OrderHom.instFunLike` `TwoSidedIdeal.asIdeal` `toTwoSided`	—	`ext`
`coe_toTwoSided` 📖	mathematical	—	`SetLike.coe` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `TwoSidedIdeal.setLike` `toTwoSided` `Ideal` `Ring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`TwoSidedIdeal.coe_mk'`
`instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided` 📖	mathematical	—	`CanLift` `Ideal` `Ring.toSemiring` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `TwoSidedIdeal.instPartialOrder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `OrderHom.instFunLike` `TwoSidedIdeal.asIdeal` `IsTwoSided`	—	`asIdeal_toTwoSided`
`mem_toTwoSided` 📖	mathematical	—	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `TwoSidedIdeal.setLike` `toTwoSided` `Ideal` `Ring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`toTwoSided_asIdeal` 📖	mathematical	—	`toTwoSided` `DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ideal` `Ring.toSemiring` `PartialOrder.toPreorder` `TwoSidedIdeal.instPartialOrder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `OrderHom.instFunLike` `TwoSidedIdeal.asIdeal` `TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal`	—	`TwoSidedIdeal.ext` `TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal`

RingEquiv

Definitions

Name	Category	Theorems
`mapTwoSidedIdeal` 📖	CompOp	2 math math: `mapTwoSidedIdeal_symm`, `mapTwoSidedIdeal_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapTwoSidedIdeal_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `TwoSidedIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `TwoSidedIdeal.instPartialOrder` `instFunLikeOrderIso` `mapTwoSidedIdeal` `OrderHom` `OrderHom.instFunLike` `TwoSidedIdeal.comap` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `instEquivLike` `symm` `RingEquivClass.toNonUnitalRingHomClass` `instRingEquivClass`	—	—
`mapTwoSidedIdeal_symm` 📖	mathematical	—	`OrderIso.symm` `TwoSidedIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `TwoSidedIdeal.instPartialOrder` `mapTwoSidedIdeal` `symm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Distrib.toAdd`	—	—

TwoSidedIdeal

Definitions

Name	Category	Theorems
`asIdeal` 📖	CompOp	12 math math: `Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided`, `instIsTwoSidedCoeOrderHomIdealAsIdeal`, `bot_asIdeal`, `Ideal.toTwoSided_asIdeal`, `asIdeal_jacobson`, `top_asIdeal`, `mem_asIdeal`, `Ideal.asIdeal_toTwoSided`, `gc`, `orderIsoIsTwoSided_apply_coe`, `asIdeal_matrix`, `coe_asIdeal`
`asIdealOpposite` 📖	CompOp	1 math math: `mem_asIdealOpposite`
`comap` 📖	CompOp	4 math math: `mem_comap`, `RingEquiv.mapTwoSidedIdeal_apply`, `comap_comap`, `comap_le_comap`
`fromIdeal` 📖	CompOp	2 math math: `mem_fromIdeal`, `gc`
`instSMulMulOppositeSubtypeMem` 📖	CompOp	1 math math: `instSMulCommClassMulOppositeSubtypeMem`
`instSMulSubtypeMem` 📖	CompOp	1 math math: `instSMulCommClassMulOppositeSubtypeMem`
`leftModule` 📖	CompOp	3 math math: `subtype_injective`, `coe_subtype`, `subtype_apply`
`map` 📖	CompOp	1 math math: `map_mono`
`orderIsoIdeal` 📖	CompOp	—
`orderIsoIsTwoSided` 📖	CompOp	2 math math: `orderIsoIsTwoSided_symm_apply`, `orderIsoIsTwoSided_apply_coe`
`rightModule` 📖	CompOp	2 math math: `subtypeMop_apply`, `subtypeMop_injective`
`span` 📖	CompOp	8 math math: `mem_span_iff_mem_addSubgroup_closure_absorbing`, `mem_span_iff_mem_addSubgroup_closure`, `span_mono`, `mem_fromIdeal`, `mem_span_iff_mem_addSubgroup_closure_nonunital`, `mem_span_iff`, `span_le`, `subset_span`
`subtype` 📖	CompOp	3 math math: `subtype_injective`, `coe_subtype`, `subtype_apply`
`subtypeMop` 📖	CompOp	2 math math: `subtypeMop_apply`, `subtypeMop_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_asIdeal` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ideal` `Ring.toSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `OrderHom.instFunLike` `asIdeal` `Bot.bot` `instBot` `Submodule.instBot`	—	—
`coe_asIdeal` 📖	mathematical	—	`SetLike.coe` `Ideal` `Ring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `OrderHom.instFunLike` `asIdeal` `setLike`	—	—
`coe_mop_smul` 📖	mathematical	—	`MulOpposite` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `MulOpposite.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toOppositeModule` `TwoSidedIdeal` `SetLike.instMembership` `setLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulOpposite.unop`	—	—
`coe_smul` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `TwoSidedIdeal` `SetLike.instMembership` `setLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `AddCommGroup.toAddCommMonoid` `addCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `leftModule` `Semiring.toModule` `LinearMap.instFunLike` `subtype`	—	—
`comap_comap` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `PartialOrder.toPreorder` `instPartialOrder` `OrderHom.instFunLike` `comap` `RingHom` `NonAssocRing.toNonAssocSemiring` `RingHom.instFunLike` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `RingHom.comp`	—	`ext` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`comap_le_comap` 📖	mathematical	`TwoSidedIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `comap`	—	`OrderHom.monotone`
`gc` 📖	mathematical	—	`GaloisConnection` `Ideal` `Ring.toSemiring` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instPartialOrder` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `fromIdeal` `asIdeal`	—	`mem_span_iff`
`instIsTwoSidedCoeOrderHomIdealAsIdeal` 📖	mathematical	—	`Ideal.IsTwoSided` `Ring.toSemiring` `DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ideal` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `OrderHom.instFunLike` `asIdeal`	—	`mul_mem_right`
`instSMulCommClassMulOppositeSubtypeMem` 📖	mathematical	—	`SMulCommClass` `MulOpposite` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `instSMulSubtypeMem` `instSMulMulOppositeSubtypeMem`	—	`SMulCommClass.smul_comm` `SMulCommClass.opposite_mid` `IsScalarTower.left`
`map_mono` 📖	mathematical	`TwoSidedIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`map`	—	`span_mono` `Set.image_mono`
`mem_asIdeal` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `OrderHom.instFunLike` `asIdeal` `setLike`	—	—
`mem_asIdealOpposite` 📖	mathematical	—	`MulOpposite` `Ideal` `MulOpposite.instSemiring` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `OrderHom.instFunLike` `asIdealOpposite` `setLike` `MulOpposite.unop`	—	`RingCon.symm`
`mem_comap` 📖	mathematical	—	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `instPartialOrder` `OrderHom.instFunLike` `comap`	—	`map_mul` `AddCon.add'` `map_add` `map_zero` `AddMonoidHomClass.toZeroHomClass` `NonUnitalRingHomClass.toAddMonoidHomClass`
`mem_fromIdeal` 📖	mathematical	—	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `DFunLike.coe` `OrderHom` `Ideal` `Ring.toSemiring` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instPartialOrder` `OrderHom.instFunLike` `fromIdeal` `span` `SetLike.coe` `Submodule.setLike`	—	—
`mem_span_iff` 📖	mathematical	—	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `span`	—	`RingCon.ringConGen_eq` `sInf_le` `rel_iff` `SetLike.mem_coe` `subset_span`
`mem_span_iff_mem_addSubgroup_closure` 📖	mathematical	—	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `span` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddSubgroup.instSetLike` `AddSubgroup.closure` `Set` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Set.univ`	—	`span_mono` `Set.mem_univ` `one_mul` `mul_one` `mem_span_iff` `subset_mul_set` `set_mul_subset` `subset_span` `mem_span_iff_mem_addSubgroup_closure_absorbing` `mul_assoc`
`mem_span_iff_mem_addSubgroup_closure_absorbing` 📖	mathematical	`Set` `Set.instMembership` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	`TwoSidedIdeal` `SetLike.instMembership` `setLike` `span` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instSetLike` `AddSubgroup.closure`	—	`AddSubgroup.mem_map_of_mem` `AddMonoidHom.map_closure` `AddSubgroup.closure_mono` `AddSubgroup.zero_mem` `AddSubgroup.add_mem` `AddSubgroup.neg_mem` `mem_span_iff` `AddSubgroup.subset_closure` `AddSubgroup.closure_induction` `zero_mem` `add_mem` `neg_mem`
`mem_span_iff_mem_addSubgroup_closure_nonunital` 📖	mathematical	—	`TwoSidedIdeal` `NonUnitalRing.toNonUnitalNonAssocRing` `SetLike.instMembership` `setLike` `span` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instSetLike` `AddSubgroup.closure` `Set` `Set.instUnion` `Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Set.univ`	—	`span_mono` `Set.union_assoc` `mem_span_iff` `subset_span` `subset_mul_set` `set_mul_subset` `mem_span_iff_mem_addSubgroup_closure_absorbing` `Set.mem_univ` `mul_assoc`
`orderIsoIsTwoSided_apply_coe` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `Ideal.IsTwoSided` `DFunLike.coe` `RelIso` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RelIso.instFunLike` `orderIsoIsTwoSided` `OrderHom` `OrderHom.instFunLike` `asIdeal`	—	—
`orderIsoIsTwoSided_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Ideal` `Ring.toSemiring` `Ideal.IsTwoSided` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `orderIsoIsTwoSided`	—	—
`set_mul_subset` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `TwoSidedIdeal` `NonUnitalRing.toNonUnitalNonAssocRing` `setLike`	`Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`mul_mem_left`
`span_induction` 📖	—	`subset_span` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `zero_mem` `span` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `add_mem` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `neg_mem` `Distrib.toMul` `mul_mem_left` `mul_mem_right` `TwoSidedIdeal` `SetLike.instMembership` `setLike`	—	—	`subset_span` `zero_mem` `add_mem` `neg_mem` `mul_mem_left` `mul_mem_right` `span_le` `sub_zero` `mem_span_iff`
`span_le` 📖	mathematical	—	`TwoSidedIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `span` `Set` `Set.instHasSubset` `SetLike.coe` `setLike`	—	`ringCon_le_iff` `GaloisInsertion.gc` `sub_zero` `rel_iff`
`span_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`TwoSidedIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `span`	—	`mem_span_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset`
`subset_mul_set` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `TwoSidedIdeal` `NonUnitalRing.toNonUnitalNonAssocRing` `setLike`	`Set.mul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`mul_mem_right`
`subset_span` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `TwoSidedIdeal` `setLike` `span`	—	`SetLike.mem_coe` `mem_iff` `sub_zero`
`subtypeMop_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `MulOpposite` `MulOpposite.instSemiring` `Ring.toSemiring` `RingHom.id` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `AddCommGroup.toAddCommMonoid` `addCommGroup` `MulOpposite.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `rightModule` `MulOpposite.instModule` `Semiring.toOppositeModule` `LinearMap.instFunLike` `subtypeMop` `MulOpposite.op`	—	—
`subtypeMop_injective` 📖	mathematical	—	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `MulOpposite` `DFunLike.coe` `LinearMap` `MulOpposite.instSemiring` `Ring.toSemiring` `RingHom.id` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommGroup` `MulOpposite.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `rightModule` `MulOpposite.instModule` `Semiring.toOppositeModule` `LinearMap.instFunLike` `subtypeMop`	—	`MulOpposite.op_injective` `Subtype.coe_injective`
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `AddCommGroup.toAddCommMonoid` `addCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `leftModule` `Semiring.toModule` `LinearMap.instFunLike` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `leftModule` `Semiring.toModule` `LinearMap.instFunLike` `subtype`	—	`Subtype.coe_injective`
`top_asIdeal` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `TwoSidedIdeal` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ideal` `Ring.toSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `OrderHom.instFunLike` `asIdeal` `Top.top` `instTop` `Submodule.instTop`	—	—

---

← Back to Index