MulOpposite

📁 Source: Mathlib/Algebra/Ring/Subsemiring/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_toSubmonoid`, `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_toSubmonoid`, `unop_top`	46
Total	52

Subsemiring

Definitions

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

Theorems

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

---

← Back to Index