[Merged by Bors] - feat: port RingTheory.Artinian

[int-y1]

---

todo:

• (optional) class IsArtinian understand this comment: "infer kinds are unsupported in Lean 4"
• instance isArtinian_pi failed to synthesize instance
• theorem isArtinian_of_fG_of_artinian application type mismatch at isArtinian_of_surjective

[ChrisHughes24]

The inferkinds error is to do with the [] in the Lean3 definition. It makes some stuff implicit or explicit, but I can't check what it does because I can't install mathlibtools right now for some reason.

class is_artinian (R M) [semiring R] [add_comm_monoid M] [module R M] : Prop :=
(well_founded_submodule_lt [] : well_founded ((<) : submodule R M → submodule R M → Prop))

[int-y1]

The type in Lean 3 is:

is_artinian.well_founded_submodule_lt : ∀ (R : Type u_1) (M : Type u_3) [_inst_1 : semiring R] [_inst_2 : add_comm_monoid M] [_inst_3 : module R M] [self : is_artinian R M], well_founded has_lt.lt

Removing [] changed the type from (R) (M) to {R} {M}.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style