Commit 2024-06-30 19:02 c1c6ecdf

feat: simple lemmas about fractional ideals (#14099) Prove five lemmas about fractional ideals (zero_mem, fg_of_isNoetherianRing, den_mem_inv, num_le_mul_inv, bot_lt_mul_inv). This is part 1/4 of a proof of isDedekindDomain_iff_isDedekindDomainDvr. Part 2: #14216 Part 3: #14237 Part 4: #14242