feat(GroupTheory/Subgroup/Basic): ker_{fst,snd} (#6639)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community · Aug 18, 2023 · 338bb3f · 338bb3f
1 parent 6c02c99
commit 338bb3f
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean
@@ -2887,6 +2887,12 @@ instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal :=
 #align monoid_hom.normal_ker MonoidHom.normal_ker
 #align add_monoid_hom.normal_ker AddMonoidHom.normal_ker
 
+@[to_additive (attr := simp)]
+lemma ker_fst : ker (fst G G') = .prod ⊥ ⊤ := SetLike.ext fun _ => (and_true_iff _).symm
+
+@[to_additive (attr := simp)]
+lemma ker_snd : ker (snd G G') = .prod ⊤ ⊥ := SetLike.ext fun _ => (true_and_iff _).symm
+
 end Ker
 
 section EqLocus

diff --git a/Mathlib/GroupTheory/Submonoid/Operations.lean b/Mathlib/GroupTheory/Submonoid/Operations.lean
@@ -1244,6 +1244,12 @@ theorem mker_inr : mker (inr M N) = ⊥ := by
 #align monoid_hom.mker_inr MonoidHom.mker_inr
 #align add_monoid_hom.mker_inr AddMonoidHom.mker_inr
 
+@[to_additive (attr := simp)]
+lemma mker_fst : mker (fst M N) = .prod ⊥ ⊤ := SetLike.ext fun _ => (and_true_iff _).symm
+
+@[to_additive (attr := simp)]
+lemma mker_snd : mker (snd M N) = .prod ⊤ ⊥ := SetLike.ext fun _ => (true_and_iff _).symm
+
 /-- The `MonoidHom` from the preimage of a submonoid to itself. -/
 @[to_additive (attr := simps)
       "the `AddMonoidHom` from the preimage of an additive submonoid to itself."]