Theorem Rat.MulRingNorm.one_lt_of_not_bounded

Modification history