Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-24 07:29 082350f2

View on Github →

feat(number_theory/padics/padic_numbers): add is_fraction_ring instance (#16981) ℚ_[p] is the fraction ring of ℤ_[p].

Estimated changes

added theorem padic_int.coe_eq_zero