MulOpposite

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean

Statistics

Metric	Count
Definitions `algEquivOpMop`, `linearEquivOp`, `mopAlgEquivOp`, `op`, `opEquiv`, `unop`	6
Theorems `algEquivOpMop_apply`, `algEquivOpMop_symm_apply_coe`, `coe_op`, `coe_unop`, `le_op_iff`, `linearEquivOp_apply_coe`, `linearEquivOp_symm_apply_coe`, `mem_op`, `mem_unop`, `mopAlgEquivOp_apply_coe`, `mopAlgEquivOp_symm_apply`, `opEquiv_apply`, `opEquiv_symm_apply`, `op_adjoin`, `op_bot`, `op_iInf`, `op_iSup`, `op_inf`, `op_le_iff`, `op_le_op_iff`, `op_sInf`, `op_sSup`, `op_sup`, `op_toSubring`, `op_toSubsemiring`, `op_top`, `op_unop`, `unop_adjoin`, `unop_bot`, `unop_iInf`, `unop_iSup`, `unop_inf`, `unop_le_unop_iff`, `unop_op`, `unop_sInf`, `unop_sSup`, `unop_sup`, `unop_toSubring`, `unop_toSubsemiring`, `unop_top`	40
Total	46

Subalgebra

Definitions

Name	Category	Theorems
`algEquivOpMop` 📖	CompOp	2 math math: `algEquivOpMop_apply`, `algEquivOpMop_symm_apply_coe`
`linearEquivOp` 📖	CompOp	2 math math: `linearEquivOp_apply_coe`, `linearEquivOp_symm_apply_coe`
`mopAlgEquivOp` 📖	CompOp	2 math math: `mopAlgEquivOp_symm_apply`, `mopAlgEquivOp_apply_coe`
`op` 📖	CompOp	29 math math: `op_toSubsemiring`, `mem_op`, `op_sSup`, `op_sInf`, `op_bot`, `LinearDisjoint.linearIndependent_left_op_of_flat`, `mopAlgEquivOp_symm_apply`, `op_adjoin`, `op_inf`, `coe_op`, `linearEquivOp_apply_coe`, `unop_sSup`, `unop_op`, `op_top`, `op_iInf`, `op_le_iff`, `algEquivOpMop_apply`, `op_toSubring`, `op_unop`, `op_iSup`, `op_sup`, `linearEquivOp_symm_apply_coe`, `le_op_iff`, `mopAlgEquivOp_apply_coe`, `LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op`, `algEquivOpMop_symm_apply_coe`, `op_le_op_iff`, `opEquiv_apply`, `unop_sInf`
`opEquiv` 📖	CompOp	2 math math: `opEquiv_symm_apply`, `opEquiv_apply`
`unop` 📖	CompOp	21 math math: `op_sSup`, `op_sInf`, `unop_sup`, `unop_top`, `unop_bot`, `unop_toSubring`, `unop_sSup`, `unop_op`, `unop_le_unop_iff`, `unop_iInf`, `unop_inf`, `mem_unop`, `unop_adjoin`, `op_le_iff`, `op_unop`, `unop_toSubsemiring`, `coe_unop`, `opEquiv_symm_apply`, `le_op_iff`, `unop_iSup`, `unop_sInf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquivOpMop_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Subalgebra` `SetLike.instMembership` `instSetLike` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `op` `toSemiring` `algebra` `AlgEquiv.instFunLike` `algEquivOpMop` `MulOpposite.op` `Subsemiring` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `Subsemiring.instSetLike` `Subsemiring.op` `toSubsemiring` `AddEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.toNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `Subsemiring.addEquivOp`	—	—
`algEquivOpMop_symm_apply_coe` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `toSubsemiring` `DFunLike.coe` `AlgEquiv` `MulOpposite` `Subalgebra` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instSetLike` `op` `toSemiring` `algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `algEquivOpMop` `MulOpposite.unop` `Submonoid` `MulOpposite.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Submonoid.op` `Subsemiring.toSubmonoid` `MulOpposite.instNonAssocSemiring` `Subsemiring.op`	—	—
`coe_op` 📖	mathematical	—	`SetLike.coe` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instSetLike` `op` `Set.preimage` `MulOpposite.unop`	—	—
`coe_unop` 📖	mathematical	—	`SetLike.coe` `Subalgebra` `instSetLike` `unop` `Set.preimage` `MulOpposite` `MulOpposite.op` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	—
`le_op_iff` 📖	mathematical	—	`Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`linearEquivOp_apply_coe` 📖	mathematical	—	`MulOpposite` `Subsemiring` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.op` `toSubsemiring` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `RingHomInvPair.ids` `Subalgebra` `instSetLike` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `op` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearEquivOp` `MulOpposite.op` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Subsemiring.toSubmonoid`	—	`RingHomInvPair.ids`
`linearEquivOp_symm_apply_coe` 📖	mathematical	—	`Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `toSubsemiring` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `RingHomInvPair.ids` `MulOpposite` `Subalgebra` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `instSetLike` `op` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearEquivOp` `MulOpposite.unop` `Submonoid` `MulOpposite.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Submonoid.op` `Subsemiring.toSubmonoid`	—	`RingHomInvPair.ids`
`mem_op` 📖	mathematical	—	`MulOpposite` `Subalgebra` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `SetLike.instMembership` `instSetLike` `op` `MulOpposite.unop`	—	—
`mem_unop` 📖	mathematical	—	`Subalgebra` `SetLike.instMembership` `instSetLike` `unop` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `MulOpposite.op`	—	—
`mopAlgEquivOp_apply_coe` 📖	mathematical	—	`MulOpposite` `Subsemiring` `MulOpposite.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.op` `toSubsemiring` `DFunLike.coe` `AlgEquiv` `Subalgebra` `instSetLike` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `op` `toSemiring` `algebra` `AlgEquiv.instFunLike` `mopAlgEquivOp` `MulOpposite.op` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike` `Subsemiring.toSubmonoid` `MulOpposite.unop`	—	—
`mopAlgEquivOp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `MulOpposite` `Subalgebra` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `SetLike.instMembership` `instSetLike` `op` `toSemiring` `algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `mopAlgEquivOp` `MulOpposite.op` `Subsemiring` `Semiring.toNonAssocSemiring` `Subsemiring.instSetLike` `toSubsemiring` `AddEquiv` `MulOpposite.instNonAssocSemiring` `Subsemiring.op` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.toNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `Subsemiring.addEquivOp`	—	—
`opEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `opEquiv` `op`	—	—
`opEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `opEquiv` `unop`	—	—
`op_adjoin` 📖	mathematical	—	`op` `Algebra.adjoin` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Set.preimage` `MulOpposite.unop`	—	`toSubsemiring_injective` `Subsemiring.op_closure` `Set.ext` `MulOpposite.op_injective` `MulOpposite.op_unop`
`op_bot` 📖	mathematical	—	`op` `Bot.bot` `Subalgebra` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	`OrderIso.map_bot`
`op_iInf` 📖	mathematical	—	`op` `iInf` `Subalgebra` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	`OrderIso.map_iInf`
`op_iSup` 📖	mathematical	—	`op` `iSup` `Subalgebra` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	`OrderIso.map_iSup`
`op_inf` 📖	mathematical	—	`op` `Subalgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	`OrderIso.map_inf`
`op_le_iff` 📖	mathematical	—	`Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op` `unop`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`op_le_op_iff` 📖	mathematical	—	`Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `op`	—	`Function.Surjective.forall` `MulOpposite.op_surjective`
`op_sInf` 📖	mathematical	—	`op` `InfSet.sInf` `Subalgebra` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Set.preimage` `unop`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`op_sSup` 📖	mathematical	—	`op` `SupSet.sSup` `Subalgebra` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Set.preimage` `unop`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`op_sup` 📖	mathematical	—	`op` `Subalgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	`OrderIso.map_sup`
`op_toSubring` 📖	mathematical	—	`toSubring` `MulOpposite` `MulOpposite.instRing` `MulOpposite.instAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `op` `Subring.op`	—	—
`op_toSubsemiring` 📖	mathematical	—	`toSubsemiring` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `op` `Subsemiring.op` `Semiring.toNonAssocSemiring`	—	—
`op_top` 📖	mathematical	—	`op` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	`OrderIso.map_top`
`op_unop` 📖	mathematical	—	`op` `unop`	—	—
`unop_adjoin` 📖	mathematical	—	`unop` `Algebra.adjoin` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Set.preimage` `MulOpposite.op`	—	`toSubsemiring_injective` `Subsemiring.unop_closure` `Set.ext`
`unop_bot` 📖	mathematical	—	`unop` `Bot.bot` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`OrderIso.map_bot`
`unop_iInf` 📖	mathematical	—	`unop` `iInf` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	—	`OrderIso.map_iInf`
`unop_iSup` 📖	mathematical	—	`unop` `iSup` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	—	`OrderIso.map_iSup`
`unop_inf` 📖	mathematical	—	`unop` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	—	`OrderIso.map_inf`
`unop_le_unop_iff` 📖	mathematical	—	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `unop` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	`Function.Surjective.forall` `MulOpposite.unop_surjective`
`unop_op` 📖	mathematical	—	`unop` `op`	—	—
`unop_sInf` 📖	mathematical	—	`unop` `InfSet.sInf` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Set.preimage` `op`	—	`OrderIso.map_sInf_eq_sInf_symm_preimage`
`unop_sSup` 📖	mathematical	—	`unop` `SupSet.sSup` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Set.preimage` `op`	—	`OrderIso.map_sSup_eq_sSup_symm_preimage`
`unop_sup` 📖	mathematical	—	`unop` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	—	`OrderIso.map_sup`
`unop_toSubring` 📖	mathematical	—	`toSubring` `unop` `CommRing.toCommSemiring` `Ring.toSemiring` `Subring.unop` `MulOpposite` `MulOpposite.instRing` `MulOpposite.instAlgebra`	—	—
`unop_toSubsemiring` 📖	mathematical	—	`toSubsemiring` `unop` `Subsemiring.unop` `Semiring.toNonAssocSemiring` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra`	—	—
`unop_top` 📖	mathematical	—	`unop` `Top.top` `Subalgebra` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`OrderIso.map_top`

---

← Back to Index