mathlib3
d20f598e - chore(ring_theory.dedekind_domain.adic_valuation): delete outdated comment (#16886)

Commit
3 years ago
chore(ring_theory.dedekind_domain.adic_valuation): delete outdated comment (#16886)
Author
Parents
Loading