Mathlib Map

Theorems · Definition · number theory

PadicInt.toZModHom

{p : ℕ} →
  [hp_prime : Fact (Nat.Prime p)] →
    (v : ℕ) →
      (f : ℤ_[p] → ℕ) →
        (∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}) →
          (∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b) → ℤ_[p] →+* ZMod v

toZModHom is an auxiliary constructor for creating ring homs from ℤ_[p] to ZMod v.

Defined in
Mathlib.NumberTheory.Padics.RingHoms
Cited by
0 results in Mathlib
Foundations
Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Fact
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PadicInt.toZModPow · cited by 17PadicInt.toZModPowPadicInt.toZMod · cited by 10PadicInt.toZModSet · cited by 53352SetRingHom · cited by 10189RingHomIdeal · cited by 4748IdealFact · cited by 2726FactNat.Prime · cited by 2059Nat.PrimeZMod · cited by 1024ZModIdeal.span · cited by 948Ideal.spanPadicInt · cited by 179PadicIntPadicInt.toZModHomCITED BYCITES

Cites8

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

  • Setstatement · cited by 53,352
  • RingHomstatement · cited by 10,189
  • Idealstatement · cited by 4,748
  • Factstatement and proof · cited by 2,726
  • Nat.Primestatement and proof · cited by 2,059
  • ZModstatement · cited by 1,024
  • Ideal.spanstatement and proof · cited by 948
  • PadicIntstatement and proof · cited by 179

Cited by2

Results whose statement or proof uses this declaration.