Theorems · Theorem · number theory
Nat.modEq_eleven_digits_sum
∀ (n : ℕ), ↑n ≡ (List.map (fun n => ↑n) (Nat.digits 10 n)).alternatingSum [ZMOD 11]
- Defined in
- Mathlib.Data.Nat.Digits.Div
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Int.ModEqstatement and proof · cited by 147
- Nat.digitsstatement and proof · cited by 70
- Nat.ofDigitsproof · cited by 61
- List.alternatingSumstatement · cited by 15
- Nat.zmodeq_ofDigits_digitsproof · cited by 2
- Nat.ofDigits_neg_oneproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.