Theorem Rat.MulRingNorm.mulRingNorm_eq_one_of_not_dvd

Modification history