Commit 2025-12-16 07:12 8ee8525c

View on Github →

chore(Algebra): consistently tag mem_sInf, mem_iInf, coe_sInf, coe_iInf (#32887)

  • Consistently tag mem_sInf, mem_iInf as simp across all algebraic substructures
  • Consistently tag coe_sInf, coe_iInf as simp, norm_cast across all algebraic substructures

Estimated changes

modified theorem Algebra.mem_iInf
modified theorem Subfield.mem_iInf
modified theorem Subgroup.mem_iInf
modified theorem Submonoid.mem_iInf
modified theorem Subsemigroup.mem_iInf
modified theorem LieSubmodule.mem_iInf
modified theorem Submodule.mem_iInf
modified theorem Subring.mem_iInf
modified theorem Subsemiring.mem_iInf