CharZero

📁 Source: Mathlib/Data/Rat/Cast/CharZero.lean

Statistics

Metric	Count
Definitions CharZero, castHom, castHom	3
Theorems cast_add, cast_div, cast_divNat, cast_eq_zero, cast_inj, cast_injective, cast_inv, cast_mul, cast_ne_zero, cast_zpow, coe_castHom, cast_add, cast_div, cast_divInt, cast_eq_zero, cast_inj, cast_injective, cast_inv, cast_mul, cast_ne_zero, cast_sub, cast_zpow, coe_castHom	23
Total	26

NNRat

Definitions

Name	Category	Theorems
castHom 📖	CompOp	1 math math: coe_castHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_add 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield	—	cast_add_of_ne_zero Nat.cast_ne_zero LT.lt.ne' den_pos
cast_div 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat instDiv DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cast_divNat 📖	mathematical	—	cast DivisionSemiring.toNNRatCast divNat DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	—	cast_natCast cast_div ext
cast_eq_zero 📖	mathematical	—	cast DivisionSemiring.toNNRatCast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring NNRat Semifield.toDivisionSemiring instSemifield	—	cast_zero
cast_inj 📖	mathematical	—	cast DivisionSemiring.toNNRatCast	—	cast_injective
cast_injective 📖	mathematical	—	NNRat cast DivisionSemiring.toNNRatCast	—	num_div_den div_eq_div_iff Nat.cast_zero instCharZero den_ne_zero Commute.div_eq_div_iff Nat.cast_commute cast_def
cast_inv 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cast_mul 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield	—	cast_mul_of_ne_zero Nat.cast_ne_zero LT.lt.ne' den_pos
cast_ne_zero 📖	—	—	—	—	Iff.not cast_eq_zero
cast_zpow 📖	mathematical	—	cast DivisionSemiring.toNNRatCast NNRat instZPow DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	map_zpow₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
coe_castHom 📖	mathematical	—	DFunLike.coe RingHom NNRat Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSemifield RingHom.instFunLike castHom cast DivisionSemiring.toNNRatCast	—	—

Rat

Definitions

Name	Category	Theorems
castHom 📖	CompOp	12 math math: CongruenceSubgroup.exists_Gamma_le_conj', coe_castHom, castHom_rat, CongruenceSubgroup.IsArithmetic.conj, Padic.comap_mulValuation_eq_padicValuation, CongruenceSubgroup.isArithmetic_conj_SL2Z, CongruenceSubgroup.finiteIndex_conjGL, Padic.isUniformInducing_cast_withVal, Padic.coe_withValRingEquiv_symm, CongruenceSubgroup.IsCongruenceSubgroup.conjGL, Padic.isDenseInducing_cast_withVal, Subgroup.IsArithmetic.conj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_add 📖	mathematical	—	DivisionRing.toRatCast Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	—	cast_add_of_ne_zero Nat.cast_ne_zero LT.lt.ne' pos
cast_div 📖	mathematical	—	DivisionRing.toRatCast DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cast_divInt 📖	mathematical	—	DivisionRing.toRatCast DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing	—	cast_div cast_intCast
cast_eq_zero 📖	mathematical	—	DivisionRing.toRatCast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	—	cast_injective cast_zero
cast_inj 📖	mathematical	—	DivisionRing.toRatCast	—	cast_injective
cast_injective 📖	mathematical	—	DivisionRing.toRatCast	—	Nat.cast_ne_zero Int.cast_mul Int.cast_natCast eq_div_iff_mul_eq division_def mul_assoc Commute.eq Commute.inv_left₀ Nat.cast_commute cast_divInt_of_ne_zero
cast_inv 📖	mathematical	—	DivisionRing.toRatCast InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cast_mul 📖	mathematical	—	DivisionRing.toRatCast Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	—	cast_mul_of_ne_zero Nat.cast_ne_zero LT.lt.ne' pos
cast_ne_zero 📖	—	—	—	—	Iff.ne cast_eq_zero
cast_sub 📖	mathematical	—	DivisionRing.toRatCast SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing	—	cast_sub_of_ne_zero Nat.cast_ne_zero LT.lt.ne' pos
cast_zpow 📖	mathematical	—	DivisionRing.toRatCast DivInvMonoid.toZPow DivisionRing.toDivInvMonoid	—	map_zpow₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
coe_castHom 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.instFunLike castHom DivisionRing.toRatCast	—	—

(root)

Definitions

Name	Category	Theorems
CharZero 📖	CompData	62 math math: WithTop.charZero, Polynomial.charZero, AddMonoidWithOne.toCharZero, Prod.charZero_of_right, CharZero.of_addMonoidHom, IntermediateField.charZero, Padic.instCharZero, algebraRat.charZero, ENNReal.instCharZero, RingHom.charZero, CharP.exists', charZero_of_inj_zero, Nat.instCharZero, CharP.ringChar_zero_iff_CharZero, MvPolynomial.instCharZero, RingHom.charZero_iff, CharZero.charZero_iff_forall_prime_ne_zero, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, NNRat.instCharZero, Cardinal.instCharZero, WithBot.charZero, Zsqrtd.instCharZero, CharP.charP_to_charZero, NumberField.RingOfIntegers.instCharZero, NumberField.finite_of_discr_bdd, RatFunc.instCharZero, Algebra.charZero_of_charZero, EqualCharZero.nonempty_algebraRat_iff, SubsemiringClass.instCharZero, Rat.instCharZero, QuadraticAlgebra.instCharZero, IsStrictOrderedRing.toCharZero, Polynomial.SplittingField.instCharZero, FreeAlgebra.charZero, EqualCharZero.iff_not_mixedCharZero, CharZero.of_isAddTorsionFree, NumberField.to_charZero, CharP.charP_zero_iff_charZero, instCharZeroOfIsSemireal, CyclotomicField.instCharZero, EqualCharZero.of_algebraRat, ZMod.charZero, charZero_of_expChar_one', Int.instCharZero, Prod.charZero_of_left, CharZero.of_module, RCLike.charZero_rclike, instCharZeroEReal, AlgebraicClosure.instCharZero, PartENat.instCharZero, NatOrdinal.instCharZero, NumberField.RingOfIntegers.instCharZero_1, charZero_of_injective_ringHom, charZero_of_injective_algebraMap, MixedCharZero.toCharZero, PadicInt.instCharZero, Complex.instCharZero, EqualCharZero.of_not_mixedCharZero, Ordinal.instCharZero, IsFractionRing.charZero, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal, IsFractionRing.charZero_of_isFractionRing

---

← Back to Index