CharZero

📁 Source: Mathlib/Algebra/Ring/CharZero.lean

Statistics

Metric	Count
Definitions castEmbedding	1
Theorems two, eq_neg_self_iff, neg_eq_self_iff, mulSupport_natCast, support_natCast, of_isCancelMulZero_charZero, castEmbedding_apply, cast_pow_eq_one, charZero, charZero_iff, injective_nat, add_self_eq_zero, nat_mul_inj, nat_mul_inj', neg_units_ne_self, units_ne_neg_self	16
Total	17

CharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_neg_self_iff 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonAssocRing.toNonUnitalNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	eq_neg_iff_add_eq_zero add_self_eq_zero
neg_eq_self_iff 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonAssocRing.toNonUnitalNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	neg_eq_iff_add_eq_zero add_self_eq_zero

CharZero.NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
two 📖	mathematical	—	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_two Nat.cast_ne_zero

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulSupport_natCast 📖	mathematical	—	mulSupport AddMonoidWithOne.toOne Pi.instNatCast AddMonoidWithOne.toNatCast Set.univ	—	mulSupport_const Nat.cast_ne_one
support_natCast 📖	mathematical	—	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid Pi.instNatCast AddMonoidWithOne.toNatCast Set.univ	—	support_const Nat.cast_ne_zero

IsAddTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isCancelMulZero_charZero 📖	mathematical	—	IsAddTorsionFree AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	nsmul_eq_mul IsCancelMulZero.toIsLeftCancelMulZero

Nat

Definitions

Name	Category	Theorems
castEmbedding 📖	CompOp	12 math math: Ioc_filter_modEq_cast, Int.divisorsAntidiag_natCast, Int.Ioo_eq_finset_map, castEmbedding_apply, Int.Icc_eq_finset_map, Int.Ioc_eq_finset_map, Ico_filter_modEq_cast, Int.uIcc_eq_finset_map, LaurentPolynomial.toLaurent_support, Int.Ico_eq_finset_map, Int.divisorsAntidiag_ofNat, Int.divisorsAntidiag_neg_natCast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
castEmbedding_apply 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding castEmbedding AddMonoidWithOne.toNatCast	—	—
cast_pow_eq_one 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring AddMonoidWithOne.toOne	—	instIsMulTorsionFree

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charZero 📖	mathematical	—	CharZero AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	CharZero.cast_injective map_natCast instRingHomClass
charZero_iff 📖	mathematical	DFunLike.coe RingHom instFunLike	CharZero AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_natCast instRingHomClass charZero
injective_nat 📖	mathematical	—	DFunLike.coe RingHom Nat.instNonAssocSemiring instFunLike	—	Nat.cast_injective Unique.instSubsingleton

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_self_eq_zero 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instAtLeastTwoHAddOfNat two_mul CharZero.NeZero.two
nat_mul_inj 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	—	Nat.cast_zero sub_eq_zero mul_eq_zero mul_sub
nat_mul_inj' 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	—	—
neg_units_ne_self 📖	—	—	—	—	units_ne_neg_self
units_ne_neg_self 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat CharZero.NeZero.two

---

← Back to Index