Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(ring_theory/submonoid/membership): generalize a few lemmas to mul_mem_class #13748

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(ring_theory/submonoid/membership): generalize a few lemmas to mul_mem_class #13748

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
019da44
generalize to `mul_mem_class`
j-loreaux Apr 27, 2022
3f77f6d
fix
j-loreaux Apr 27, 2022
ec7f7c4
fix
j-loreaux Apr 27, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 12 additions & 7 deletions src/group_theory/submonoid/membership.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -457,20 +457,21 @@ attribute [to_additive add_submonoid.multiples_subset] submonoid.powers_subset

end add_submonoid

/-! Lemmas about additive closures of `submonoid`. -/
namespace submonoid
/-! Lemmas about additive closures of `subsemigroup`. -/
namespace mul_mem_class

variables {R : Type*} [non_assoc_semiring R] (S : submonoid R) {a b : R}
variables {R : Type*} [non_unital_non_assoc_semiring R] [set_like M R] [mul_mem_class M R]
{S : M} {a b : R}

/-- The product of an element of the additive closure of a multiplicative submonoid `M`
/-- The product of an element of the additive closure of a multiplicative subsemigroup `M`
and an element of `M` is contained in the additive closure of `M`. -/
lemma mul_right_mem_add_closure
(ha : a ∈ add_submonoid.closure (S : set R)) (hb : b ∈ S) :
a * b ∈ add_submonoid.closure (S : set R) :=
begin
revert b,
refine add_submonoid.closure_induction ha _ _ _; clear ha a,
{ exact λ r hr b hb, add_submonoid.mem_closure.mpr (λ y hy, hy (S.mul_mem hr hb)) },
{ exact λ r hr b hb, add_submonoid.mem_closure.mpr (λ y hy, hy (mul_mem hr hb)) },
{ exact λ b hb, by simp only [zero_mul, (add_submonoid.closure (S : set R)).zero_mem] },
{ simp_rw add_mul,
exact λ r s hr hs b hb, (add_submonoid.closure (S : set R)).add_mem (hr hb) (hs hb) }
Expand All @@ -484,7 +485,7 @@ lemma mul_mem_add_closure
begin
revert a,
refine add_submonoid.closure_induction hb _ _ _; clear hb b,
{ exact λ r hr b hb, S.mul_right_mem_add_closure hb hr },
{ exact λ r hr b hb, mul_mem_class.mul_right_mem_add_closure hb hr },
{ exact λ b hb, by simp only [mul_zero, (add_submonoid.closure (S : set R)).zero_mem] },
{ simp_rw mul_add,
exact λ r s hr hs b hb, (add_submonoid.closure (S : set R)).add_mem (hr hb) (hs hb) }
Expand All @@ -494,7 +495,11 @@ end
submonoid `S` is contained in the additive closure of `S`. -/
lemma mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ add_submonoid.closure (S : set R)) :
a * b ∈ add_submonoid.closure (S : set R) :=
S.mul_mem_add_closure (add_submonoid.mem_closure.mpr (λ sT hT, hT ha)) hb
mul_mem_add_closure (add_submonoid.mem_closure.mpr (λ sT hT, hT ha)) hb

end mul_mem_class

namespace submonoid

/-- An element is in the closure of a two-element set if it is a linear combination of those two
elements. -/
Expand Down
2 changes: 1 addition & 1 deletion src/ring_theory/subsemiring/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -582,7 +582,7 @@ namespace submonoid
/-- The additive closure of a submonoid is a subsemiring. -/
def subsemiring_closure (M : submonoid R) : subsemiring R :=
{ one_mem' := add_submonoid.mem_closure.mpr (λ y hy, hy M.one_mem),
mul_mem' := λ x y, M.mul_mem_add_closure,
mul_mem' := λ x y, mul_mem_class.mul_mem_add_closure,
..add_submonoid.closure (M : set R)}

lemma subsemiring_closure_coe :
Expand Down