Opposite

📁 Source: Mathlib/Algebra/MonoidAlgebra/Opposite.lean

Statistics

Metric	Count
Definitions opRingEquiv, opRingEquiv	2
Theorems opRingEquiv_apply, opRingEquiv_single, opRingEquiv_symm_apply, opRingEquiv_symm_single, opRingEquiv_apply, opRingEquiv_single, opRingEquiv_symm_apply, opRingEquiv_symm_single	8
Total	10

AddMonoidAlgebra

Definitions

Name	Category	Theorems
opRingEquiv 📖	CompOp	4 math math: opRingEquiv_symm_single, opRingEquiv_symm_apply, opRingEquiv_single, opRingEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite AddMonoidAlgebra AddOpposite MulOpposite.instSemiring MulOpposite.instMul instMul AddOpposite.instAdd MulOpposite.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike opRingEquiv Finsupp.equivMapDomain AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddOpposite.opEquiv Finsupp.mapRange MulOpposite.op MulOpposite.opAddEquiv MulOpposite.unop Finsupp	—	—
opRingEquiv_single 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite AddMonoidAlgebra AddOpposite MulOpposite.instSemiring MulOpposite.instMul instMul AddOpposite.instAdd MulOpposite.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike opRingEquiv MulOpposite.op single AddOpposite.op	—	Finsupp.mapRange_single Finsupp.equivMapDomain_single
opRingEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv AddMonoidAlgebra MulOpposite AddOpposite MulOpposite.instSemiring instMul AddOpposite.instAdd MulOpposite.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring MulOpposite.instAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm opRingEquiv MulOpposite.op Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.mapRange MulOpposite.instAddCommMonoid MulOpposite.unop AddEquiv.symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup MulOpposite.opAddEquiv Finsupp.equivMapDomain Equiv.symm AddOpposite.opEquiv	—	Finsupp.mapRange.congr_simp Finsupp.domCongr_symm
opRingEquiv_symm_single 📖	mathematical	—	DFunLike.coe RingEquiv AddMonoidAlgebra MulOpposite AddOpposite MulOpposite.instSemiring instMul AddOpposite.instAdd MulOpposite.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring MulOpposite.instAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm opRingEquiv single MulOpposite.op AddOpposite.unop MulOpposite.unop	—	opRingEquiv_symm_apply Finsupp.mapRange.congr_simp Finsupp.equivMapDomain_single Finsupp.mapRange_single

MonoidAlgebra

Definitions

Name	Category	Theorems
opRingEquiv 📖	CompOp	4 math math: opRingEquiv_single, opRingEquiv_symm_apply, opRingEquiv_symm_single, opRingEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite MonoidAlgebra MulOpposite.instSemiring MulOpposite.instMul instMul MulOpposite.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike opRingEquiv Finsupp.equivMapDomain AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.opEquiv Finsupp.mapRange MulOpposite.op MulOpposite.opAddEquiv MulOpposite.unop Finsupp	—	—
opRingEquiv_single 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite MonoidAlgebra MulOpposite.instSemiring MulOpposite.instMul instMul MulOpposite.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike opRingEquiv MulOpposite.op single	—	Finsupp.mapRange_single Finsupp.equivMapDomain_single
opRingEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv MonoidAlgebra MulOpposite MulOpposite.instSemiring instMul MulOpposite.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring MulOpposite.instAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm opRingEquiv MulOpposite.op Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.mapRange MulOpposite.instAddCommMonoid MulOpposite.unop AddEquiv.symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup MulOpposite.opAddEquiv Finsupp.equivMapDomain Equiv.symm MulOpposite.opEquiv	—	Finsupp.mapRange.congr_simp Finsupp.domCongr_symm
opRingEquiv_symm_single 📖	mathematical	—	DFunLike.coe RingEquiv MonoidAlgebra MulOpposite MulOpposite.instSemiring instMul MulOpposite.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring MulOpposite.instAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm opRingEquiv single MulOpposite.op MulOpposite.unop	—	opRingEquiv_symm_apply Finsupp.mapRange.congr_simp Finsupp.equivMapDomain_single Finsupp.mapRange_single

---

← Back to Index