padic_numbers): add is_fraction_ring instance (#16981)

Commit

3 years ago

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

Author

mariainesdff

Parents