Theorems · Theorem · number theory
Padic.isDenseInducing_cast_withVal
∀ {p : ℕ} [inst : Fact (Nat.Prime p)],
IsDenseInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)- Defined in
- Mathlib.NumberTheory.Padics.WithVal
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- RingHomstatement · cited by 10,189
- Factstatement and proof · cited by 2,726
- Nat.Primestatement and proof · cited by 2,059
- closureproof · cited by 1,254
- RingHom.compstatement · cited by 899
- Multiplicativestatement · cited by 875
- WithZerostatement · cited by 586
- Padicstatement and proof · cited by 151
- WithValstatement · cited by 151
- RingEquiv.toRingHomstatement · cited by 150
- IsDenseInducingstatement · cited by 56
Cited by2
Results whose statement or proof uses this declaration.
- Padic.withValRingEquivproof · cited by 3
- Padic.coe_withValRingEquiv_symmstatement · cited by 0