Commit 2023-01-04 10:07 f46ac6ed

View on Github →

feat: port GroupTheory.Subsemigroup.Membership (#1318)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subsemigroup/Membership.lean

added theorem Subsemigroup.coe_supᵢ_of_directed

added theorem Subsemigroup.coe_supₛ_of_directed_on

added theorem Subsemigroup.mem_sup_left

added theorem Subsemigroup.mem_sup_right

added theorem Subsemigroup.mem_supᵢ_of_directed

added theorem Subsemigroup.mem_supᵢ_of_mem

added theorem Subsemigroup.mem_supₛ_of_directed_on

added theorem Subsemigroup.mem_supₛ_of_mem

added theorem Subsemigroup.mul_mem_sup

added theorem Subsemigroup.supᵢ_induction'

added theorem Subsemigroup.supᵢ_induction