Commit 2024-11-14 19:40 fd96b564

View on Github →

chore(RingTheory/Ideal): split off material on nonunits (#19035) I noticed (using the hoard factor calculator) that the definition of LocalRing doesn't need anything like the amount of transitive imports that RingTheory.Ideal.Basic brings in, and nonunits is barely an ideal-related definition anyway. So splitting it off from Basic seems to be the obvious move here.

Estimated changes

deleted theorem coe_subset_nonunits
deleted theorem map_mem_nonunits_iff
deleted theorem mem_nonunits_iff
deleted theorem mul_mem_nonunits_left
deleted theorem mul_mem_nonunits_right
deleted def nonunits
deleted theorem one_not_mem_nonunits
deleted theorem zero_mem_nonunits
added theorem coe_subset_nonunits
added theorem map_mem_nonunits_iff
added theorem mem_nonunits_iff
added theorem mul_mem_nonunits_left
added theorem mul_mem_nonunits_right
added def nonunits
added theorem one_not_mem_nonunits
added theorem zero_mem_nonunits