Skip to content

[Merged by Bors] - doc(RingTheory/Extension/Generators): fix docstring variable name mismatch#39705

Closed
justus-springer wants to merge 2 commits into
leanprover-community:masterfrom
justus-springer:justus/Algebra.Generators_doc_typo
Closed

[Merged by Bors] - doc(RingTheory/Extension/Generators): fix docstring variable name mismatch#39705
justus-springer wants to merge 2 commits into
leanprover-community:masterfrom
justus-springer:justus/Algebra.Generators_doc_typo

Commits

Commits on May 22, 2026