Projects by Quarter

theorem ACC_iff_all_ideals_fg (R) [comm_ring R] : ACC R ↔ all_ideals_fg R :=
begin
  constructor,
  { intros h I,
    by_contra h',
    have asc := ascending_chain_of_generators_in_not_fg_ideal I h',
    have := h (ascending_chain_of_ideals_in_not_fg_ideal I h') _,
    { cases this with N H,
      specialize H (N + 1) (by linarith),
      dsimp [ascending_chain_of_ideals_in_not_fg_ideal] at H,