Theorem exists_max_ideal_of_mem_nonunits

Modification history