Commit 2026-04-27 15:18 7a29de1a

View on Github →

chore(FieldTheory/Galois/IsGaloisGroup): fix shadowed variable declarations (#38479) In IsGaloisGroup.lean, the global variable H : Type* was being shadowed by H : Subgroup G declared later in the same scope. This PR:

  • renames the global H : Type* to G' (with corresponding updates to mulEquivCongr and mulEquivCongr_apply_smul)
  • removes the redundant redeclaration of H : Subgroup G in section Quotient :robot: Prepared with Claude Code

Estimated changes