Commit 2026-04-14 13:51 840dee58

View on Github →

feat(RingTheory/Finiteness): Improve fg_induction (#37484)

  • include the FG-hypothesis into motive for fg_induction. This is necessary, since it might be that P (M₁ ⊔ M₂) is only provable from P M₁and P M₂ if we can use that M₁ and M₂ are FG. Also, M₁.FG and M₂.FG are not provable from (M₁ ⊔ M₂).FG in general. This also enables the use of the induction tactic with fg_induction.
  • add fg_sup_span_induction that adds one 1-dimensional submodule at a time.
  • give expressive names to the induction start and induction step hypotheses.

Estimated changes

modified theorem Submodule.fg_induction