From 338bb3fb605968650667a90deeaa666d95fff36a Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Fri, 18 Aug 2023 18:30:58 +0000 Subject: [PATCH] feat(GroupTheory/Subgroup/Basic): ker_{fst,snd} (#6639) Co-authored-by: Yakov Pechersky Co-authored-by: Eric Wieser --- Mathlib/GroupTheory/Subgroup/Basic.lean | 6 ++++++ Mathlib/GroupTheory/Submonoid/Operations.lean | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean index 26ff027bf370d..9fa8bc89c8d28 100644 --- 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 index cb42d9d2c0dc2..8a17e95a2acd1 100644 --- 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."]