Commit 2025-08-28 00:23 9bab13bf

View on Github →

feat(Algebra/Group): add theorems about Submonoid.pi (#28665) This PR adds theorems on Submonoid.pi, which are the same theorems on Subgroup.pi. Also chore:

  1. moved Submonoid.pi from Subgroup/Basic.lean to Submonoid/Operations.lean, which is a more suitable place.
  2. changed the type of Subgroup.le_pi_iff, to align with its simp normal form in Set (see Set.image_subset_iff).

Estimated changes

deleted def Submonoid.pi
added theorem Submonoid.coe_pi
added theorem Submonoid.le_pi_iff
added theorem Submonoid.mem_pi
added def Submonoid.pi
added theorem Submonoid.pi_bot
added theorem Submonoid.pi_empty
added theorem Submonoid.pi_top
added theorem Set.subset_pi_iff
added theorem Set.update_mem_pi_iff