Conjneg

📁 Source: Mathlib/Algebra/Star/Conjneg.lean

Statistics

Metric	Count
Definitions conjneg, conjnegRingHom	2
Theorems conjnegRingHom_apply, conjneg_add, conjneg_apply, conjneg_bijective, conjneg_conj, conjneg_conjneg, conjneg_eq_one, conjneg_eq_zero, conjneg_inj, conjneg_injective, conjneg_involutive, conjneg_mul, conjneg_ne_conjneg, conjneg_ne_one, conjneg_ne_zero, conjneg_neg, conjneg_one, conjneg_prod, conjneg_sub, conjneg_sum, conjneg_surjective, conjneg_zero, sum_conjneg, support_conjneg	24
Total	26

(root)

Definitions

Name	Category	Theorems
conjneg 📖	CompOp	25 math math: conjneg_add, conjneg_injective, conjneg_conj, conjneg_one, conjneg_bijective, conjneg_pos, conjneg_neg, conjneg_prod, conjneg_zero, conjneg_nonpos, conjneg_sub, conjneg_eq_one, conjneg_sum, conjneg_eq_zero, conjneg_involutive, conjneg_conjneg, conjneg_surjective, conjnegRingHom_apply, conjneg_apply, conjneg_mul, conjneg_nonneg, support_conjneg, conjneg_inj, conjneg_neg', sum_conjneg
conjnegRingHom 📖	CompOp	1 math math: conjnegRingHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjnegRingHom_apply 📖	mathematical	—	DFunLike.coe RingHom Pi.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike conjnegRingHom conjneg	—	—
conjneg_add 📖	mathematical	—	conjneg Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
conjneg_apply 📖	mathematical	—	conjneg DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike starRingEnd NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
conjneg_bijective 📖	mathematical	—	Function.Bijective conjneg	—	Function.Involutive.bijective conjneg_involutive
conjneg_conj 📖	mathematical	—	conjneg DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.commSemiring RingHom.instFunLike starRingEnd Pi.instStarRingForall NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring	—	—
conjneg_conjneg 📖	mathematical	—	conjneg	—	neg_neg RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd
conjneg_eq_one 📖	mathematical	—	conjneg Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	conjneg_conjneg conjneg_one
conjneg_eq_zero 📖	mathematical	—	conjneg Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	conjneg_conjneg conjneg_zero
conjneg_inj 📖	mathematical	—	conjneg	—	conjneg_injective
conjneg_injective 📖	mathematical	—	conjneg	—	Function.Involutive.injective conjneg_involutive
conjneg_involutive 📖	mathematical	—	Function.Involutive conjneg	—	conjneg_conjneg
conjneg_mul 📖	mathematical	—	conjneg Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
conjneg_ne_conjneg 📖	—	—	—	—	conjneg_injective
conjneg_ne_one 📖	—	—	—	—	Iff.not conjneg_eq_one
conjneg_ne_zero 📖	—	—	—	—	Iff.not conjneg_eq_zero
conjneg_neg 📖	mathematical	—	conjneg CommRing.toCommSemiring Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
conjneg_one 📖	mathematical	—	conjneg Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
conjneg_prod 📖	mathematical	—	conjneg Finset.prod Pi.commMonoid CommSemiring.toCommMonoid	—	Finset.prod_apply map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.prod_congr
conjneg_sub 📖	mathematical	—	conjneg CommRing.toCommSemiring Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
conjneg_sum 📖	mathematical	—	conjneg Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Finset.sum_apply map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr
conjneg_surjective 📖	mathematical	—	conjneg	—	Function.Involutive.surjective conjneg_involutive
conjneg_zero 📖	mathematical	—	conjneg Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
sum_conjneg 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.univ conjneg DFunLike.coe RingHom RingHom.instFunLike starRingEnd	—	Fintype.sum_equiv
support_conjneg 📖	mathematical	—	Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring conjneg Set InvolutiveNeg.toNeg Set.involutiveNeg SubtractionMonoid.toInvolutiveNeg AddGroup.toSubtractionMonoid	—	Set.ext

---

← Back to Index