Mathlib Map

Theorems · Theorem · commutative algebra

CharP.natCast_eq_natCast

∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R], ↑a = ↑b ↔ a ≡ b [MOD p]
Defined in
Mathlib.Algebra.CharP.Basic
Cited by
1 results in Mathlib
Foundations
Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddMonoidWithOneCharPIsRightCancelAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CharP.natCast_injOn_Iio · cited by 5CharP.natCast_injOn_Iiozero_add · cited by 2366zero_addNat.cast_add · cited by 586Nat.cast_addCharP · cited by 478CharPAddMonoidWithOne · cited by 313AddMonoidWithOneNat.ModEq · cited by 225Nat.ModEqle_of_not_ge · cited by 72le_of_not_geIsRightCancelAdd · cited by 69IsRightCancelAddCharP.cast_eq_zero_iff · cited by 42CharP.cast_eq_zero_iffadd_right_cancel_iff · cited by 19add_right_cancel_iffNat.modEq_iff_dvd' · cited by 11Nat.modEq_iff_dvd'Nat.ModEq.comm · cited by 11ModEq.commCharP.natCast_eq_natCastCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.