Mathlib v3 is deprecated. Go to Mathlib v4

Theorem irrational_nrt_of_n_not_dvd_multiplicity

Modification history