CharZero

📁 Source: Mathlib/Data/Int/CharZero.lean

Statistics

Metric	Count
Definitions	0
Theorems mulSupport_intCast, support_intCast, cast_div_charZero, cast_div_ofNat_charZero, injective_int	5
Total	5

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulSupport_intCast 📖	mathematical	—	mulSupport AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Pi.instIntCast AddGroupWithOne.toIntCast Set.univ	—	mulSupport_const Int.cast_ne_one
support_intCast 📖	mathematical	—	support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddGroupWithOne.toAddGroup Pi.instIntCast AddGroupWithOne.toIntCast Set.univ	—	support_const Int.cast_ne_zero

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_div_charZero 📖	mathematical	—	AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	eq_or_ne cast_zero div_zero cast_div cast_ne_zero
cast_div_ofNat_charZero 📖	mathematical	—	AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	cast_div_charZero cast_natCast

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_int 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring Int.instSemiring NonAssocRing.toNonAssocSemiring instFunLike	—	Int.cast_injective Int.subsingleton_ringHom

---

← Back to Index