MulOpposite

📁 Source: Mathlib/Algebra/Ring/Subring/MulOpposite.lean

Statistics

Metric	Count
Definitions `addEquivOp`, `mopRingEquivOp`, `op`, `opEquiv`, `ringEquivOpMop`, `unop`	6
Theorems `addEquivOp_apply_coe`, `addEquivOp_symm_apply_coe`, `coe_op`, `coe_unop`, `le_op_iff`, `mem_op`, `mem_unop`, `mopRingEquivOp_apply_coe`, `mopRingEquivOp_symm_apply`, `opEquiv_apply`, `opEquiv_symm_apply`, `op_bot`, `op_closure`, `op_eq_bot`, `op_eq_top`, `op_iInf`, `op_iSup`, `op_inf`, `op_inj`, `op_injective`, `op_le_iff`, `op_le_op_iff`, `op_sInf`, `op_sSup`, `op_sup`, `op_toSubsemiring`, `op_top`, `op_unop`, `ringEquivOpMop_apply`, `ringEquivOpMop_symm_apply_coe`, `unop_bot`, `unop_closure`, `unop_eq_bot`, `unop_eq_top`, `unop_iInf`, `unop_iSup`, `unop_inf`, `unop_inj`, `unop_injective`, `unop_le_unop_iff`, `unop_op`, `unop_sInf`, `unop_sSup`, `unop_sup`, `unop_toSubsemiring`, `unop_top`	46
Total	52

Subring

Definitions

Name	Category	Theorems
`addEquivOp` 📖	CompOp	2 math math: `addEquivOp_apply_coe`, `addEquivOp_symm_apply_coe`
`mopRingEquivOp` 📖	CompOp	2 math math: `mopRingEquivOp_apply_coe`, `mopRingEquivOp_symm_apply`
`op` 📖	CompOp	31 math math: `addEquivOp_apply_coe`, `coe_op`, `op_le_op_iff`, `le_op_iff`, `op_sup`, `mopRingEquivOp_apply_coe`, `op_injective`, `op_bot`, `op_sSup`, `op_top`, `mopRingEquivOp_symm_apply`, `op_iInf`, `op_sInf`, `unop_sInf`, `mem_op`, `op_eq_bot`, `op_le_iff`, `op_inj`, `op_toSubsemiring`, `Subalgebra.op_toSubring`, `ringEquivOpMop_symm_apply_coe`, `op_iSup`, `opEquiv_apply`, `op_closure`, `op_inf`, `op_eq_top`, `unop_op`, `unop_sSup`, `ringEquivOpMop_apply`, `op_unop`, `addEquivOp_symm_apply_coe`
`opEquiv` 📖	CompOp	2 math math: `opEquiv_apply`, `opEquiv_symm_apply`
`ringEquivOpMop` 📖	CompOp	2 math math: `ringEquivOpMop_symm_apply_coe`, `ringEquivOpMop_apply`
`unop` 📖	CompOp	25 math math: `coe_unop`, `le_op_iff`, `unop_injective`, `unop_top`, `op_sSup`, `Subalgebra.unop_toSubring`, `op_sInf`, `unop_eq_top`, `unop_sInf`, `mem_unop`, `unop_le_unop_iff`, `unop_inf`, `op_le_iff`, `unop_eq_bot`, `unop_bot`, `unop_inj`, `unop_closure`, `unop_toSubsemiring`, `unop_sup`, `opEquiv_symm_apply`, `unop_iInf`, `unop_iSup`, `unop_op`, `unop_sSup`, `op_unop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquivOp_apply_coe` 📖	mathematical	—	`MulOpposite` `Submonoid` `MulOpposite.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.op` `Subsemiring.toSubmonoid` `toSubsemiring` `DFunLike.coe` `AddEquiv` `Subring` `instSetLike` `MulOpposite.instRing` `op` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOp` `MulOpposite.op`	—	—
`addEquivOp_symm_apply_coe` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Subsemiring.toSubmonoid` `toSubsemiring` `DFunLike.coe` `AddEquiv` `MulOpposite` `Subring` `MulOpposite.instRing` `instSetLike` `op` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquivOp` `MulOpposite.unop` `MulOpposite.instMulOneClass` `Submonoid.op`	—	—
`coe_op` 📖	mathematical	—	`SetLike.coe` `Subring` `MulOpposite` `MulOpposite.instRing` `instSetLike` `op` `Set.preimage` `MulOpposite.unop`	—	—
`coe_unop` 📖	mathematical	—	`SetLike.coe` `Subring` `instSetLike` `unop` `Set.preimage` `MulOpposite` `MulOpposite.op` `MulOpposite.instRing`	—	—
`le_op_iff` 📖	mathematical	—	`Subring` `MulOpposite` `MulOpposite.instRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`mem_op` 📖	mathematical	—	`MulOpposite` `Subring` `MulOpposite.instRing` `SetLike.instMembership` `instSetLike` `op` `MulOpposite.unop`	—	—
`mem_unop` 📖	mathematical	—	`Subring` `SetLike.instMembership` `instSetLike` `unop` `MulOpposite` `MulOpposite.instRing` `MulOpposite.op`	—	—
`mopRingEquivOp_apply_coe` 📖	mathematical	—	`MulOpposite` `Subsemiring` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.op` `toSubsemiring` `DFunLike.coe` `RingEquiv` `Subring` `instSetLike` `MulOpposite.instRing` `op` `MulOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `MulOpposite.instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mopRingEquivOp` `MulOpposite.op` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Subsemiring.toSubmonoid` `MulOpposite.unop`	—	—
`mopRingEquivOp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MulOpposite` `Subring` `MulOpposite.instRing` `SetLike.instMembership` `instSetLike` `op` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `MulOpposite.instMul` `Distrib.toAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `mopRingEquivOp` `MulOpposite.op` `Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instSetLike` `toSubsemiring` `AddEquiv` `MulOpposite.instNonAssocSemiring` `Subsemiring.op` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.toNonAssocSemiring` `AddEquiv.instEquivLike` `AddEquiv.symm` `Subsemiring.addEquivOp`	—	—
`opEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subring` `MulOpposite` `MulOpposite.instRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `opEquiv` `op`	—	—
`opEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subring` `MulOpposite` `MulOpposite.instRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `opEquiv` `unop`	—	—
`op_bot` 📖	mathematical	—	`op` `Bot.bot` `Subring` `instBot` `MulOpposite` `MulOpposite.instRing`	—	`OrderIso.map_bot`
`op_closure` 📖	mathematical	—	`op` `closure` `MulOpposite` `MulOpposite.instRing` `Set.preimage` `MulOpposite.unop`	—	`op_sInf` `Function.Surjective.forall` `MulOpposite.unop_surjective`
`op_eq_bot` 📖	mathematical	—	`op` `Bot.bot` `Subring` `MulOpposite` `MulOpposite.instRing` `instBot`	—	`op_injective` `op_bot`
`op_eq_top` 📖	mathematical	—	`op` `Top.top` `Subring` `MulOpposite` `MulOpposite.instRing` `instTop`	—	`op_injective` `op_top`
`op_iInf` 📖	mathematical	—	`op` `iInf` `Subring` `instInfSet` `MulOpposite` `MulOpposite.instRing`	—	`OrderIso.map_iInf`
`op_iSup` 📖	mathematical	—	`op` `iSup` `Subring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `MulOpposite` `MulOpposite.instRing`	—	`OrderIso.map_iSup`
`op_inf` 📖	mathematical	—	`op` `Subring` `instMin` `MulOpposite` `MulOpposite.instRing`	—	—
`op_inj` 📖	mathematical	—	`op`	—	`RelIso.eq_iff_eq`
`op_injective` 📖	mathematical	—	`Subring` `MulOpposite` `MulOpposite.instRing` `op`	—	`OrderIso.injective`
`op_le_iff` 📖	mathematical	—	`Subring` `MulOpposite` `MulOpposite.instRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`op_le_op_iff` 📖	mathematical	—	`Subring` `MulOpposite` `MulOpposite.instRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`op_sInf` 📖	mathematical	—	`op` `InfSet.sInf` `Subring` `instInfSet` `MulOpposite` `MulOpposite.instRing` `Set.preimage` `unop`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`op_sSup` 📖	mathematical	—	`op` `SupSet.sSup` `Subring` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `MulOpposite` `MulOpposite.instRing` `Set.preimage` `unop`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`op_sup` 📖	mathematical	—	`op` `Subring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `MulOpposite` `MulOpposite.instRing`	—	`OrderIso.map_sup`
`op_toSubsemiring` 📖	mathematical	—	`toSubsemiring` `MulOpposite` `MulOpposite.instRing` `op` `Subsemiring.op` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	—	—
`op_top` 📖	mathematical	—	`op` `Top.top` `Subring` `instTop` `MulOpposite` `MulOpposite.instRing`	—	—
`op_unop` 📖	mathematical	—	`op` `unop`	—	—
`ringEquivOpMop_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Subring` `SetLike.instMembership` `instSetLike` `MulOpposite` `MulOpposite.instRing` `op` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `MulOpposite.instMul` `Distrib.toAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `ringEquivOpMop` `MulOpposite.op` `Subsemiring` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subsemiring.instSetLike` `Subsemiring.op` `toSubsemiring` `AddEquiv` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.toNonAssocSemiring` `AddEquiv.instEquivLike` `Subsemiring.addEquivOp`	—	—
`ringEquivOpMop_symm_apply_coe` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `toSubsemiring` `DFunLike.coe` `RingEquiv` `MulOpposite` `Subring` `MulOpposite.instRing` `instSetLike` `op` `MulOpposite.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `MulOpposite.instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `ringEquivOpMop` `MulOpposite.unop` `Submonoid` `MulOpposite.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Submonoid.op` `Subsemiring.toSubmonoid` `MulOpposite.instNonAssocSemiring` `Subsemiring.op`	—	—
`unop_bot` 📖	mathematical	—	`unop` `Bot.bot` `Subring` `MulOpposite` `MulOpposite.instRing` `instBot`	—	`OrderIso.map_bot`
`unop_closure` 📖	mathematical	—	`unop` `closure` `MulOpposite` `MulOpposite.instRing` `Set.preimage` `MulOpposite.op`	—	`op_unop` `op_closure` `Set.preimage_preimage`
`unop_eq_bot` 📖	mathematical	—	`unop` `Bot.bot` `Subring` `instBot` `MulOpposite` `MulOpposite.instRing`	—	`unop_injective` `unop_bot`
`unop_eq_top` 📖	mathematical	—	`unop` `Top.top` `Subring` `instTop` `MulOpposite` `MulOpposite.instRing`	—	`unop_injective` `unop_top`
`unop_iInf` 📖	mathematical	—	`unop` `iInf` `Subring` `MulOpposite` `MulOpposite.instRing` `instInfSet`	—	`OrderIso.map_iInf`
`unop_iSup` 📖	mathematical	—	`unop` `iSup` `Subring` `MulOpposite` `MulOpposite.instRing` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice`	—	`OrderIso.map_iSup`
`unop_inf` 📖	mathematical	—	`unop` `Subring` `MulOpposite` `MulOpposite.instRing` `instMin`	—	—
`unop_inj` 📖	mathematical	—	`unop`	—	`RelIso.eq_iff_eq`
`unop_injective` 📖	mathematical	—	`Subring` `MulOpposite` `MulOpposite.instRing` `unop`	—	`OrderIso.injective`
`unop_le_unop_iff` 📖	mathematical	—	`Subring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `unop` `MulOpposite` `MulOpposite.instRing`	—	`Function.Surjective.forall` `MulOpposite.unop_surjective`
`unop_op` 📖	mathematical	—	`unop` `op`	—	—
`unop_sInf` 📖	mathematical	—	`unop` `InfSet.sInf` `Subring` `MulOpposite` `MulOpposite.instRing` `instInfSet` `Set.preimage` `op`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`unop_sSup` 📖	mathematical	—	`unop` `SupSet.sSup` `Subring` `MulOpposite` `MulOpposite.instRing` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `Set.preimage` `op`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`unop_sup` 📖	mathematical	—	`unop` `Subring` `MulOpposite` `MulOpposite.instRing` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice`	—	`OrderIso.map_sup`
`unop_toSubsemiring` 📖	mathematical	—	`toSubsemiring` `unop` `Subsemiring.unop` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `MulOpposite` `MulOpposite.instRing`	—	—
`unop_top` 📖	mathematical	—	`unop` `Top.top` `Subring` `MulOpposite` `MulOpposite.instRing` `instTop`	—	—

---

← Back to Index