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(*/Pointwise): generalize some lemmas to SMulZeroClass #9243

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(*/Pointwise): generalize some lemmas to SMulZeroClass #9243

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
3174ccc
feat(*/Pointwise): generalize some lemmas to `SMulZeroClass`
urkud Dec 23, 2023
114377b
Merge branch 'master' into YK-smul-zero
urkud Dec 28, 2023
85b87c8
Revert unnecessary changes
urkud Dec 28, 2023
cb6fdb0
Update Mathlib/Data/Finset/Pointwise.lean
urkud Dec 28, 2023
0bfd274
Update Mathlib/Data/Finset/Pointwise.lean
urkud Dec 28, 2023
86ff46c
Update Mathlib/Data/Set/Pointwise/SMul.lean
urkud Dec 29, 2023
f274c25
Update Mathlib/Data/Finset/Pointwise.lean
urkud Dec 29, 2023
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
41 changes: 25 additions & 16 deletions Mathlib/Data/Finset/Pointwise.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ pointwise subtraction

open Function MulOpposite

open BigOperators Pointwise
open scoped BigOperators Pointwise

variable {F α β γ : Type*}

Expand Down Expand Up @@ -2084,24 +2084,41 @@ lemma inv_op_smul_finset_distrib (a : α) (s : Finset α) : (op a • s)⁻¹ =

end Group

section SMulZeroClass

variable [Zero β] [SMulZeroClass α β] [DecidableEq β] {s : Finset α} {t : Finset β}

theorem smul_zero_subset (s : Finset α) : s • (0 : Finset β) ⊆ 0 := by simp [subset_iff, mem_smul]
#align finset.smul_zero_subset Finset.smul_zero_subset

theorem Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Finset β) = 0 :=
s.smul_zero_subset.antisymm <| by simpa [mem_smul] using hs
#align finset.nonempty.smul_zero Finset.Nonempty.smul_zero

theorem zero_mem_smul_finset {t : Finset β} {a : α} (h : (0 : β) ∈ t) : (0 : β) ∈ a • t :=
urkud marked this conversation as resolved.
Show resolved Hide resolved
mem_smul_finset.2 ⟨0, h, smul_zero _⟩
#align finset.zero_mem_smul_finset Finset.zero_mem_smul_finset

variable [Zero α] [NoZeroSMulDivisors α β] {a : α}

theorem zero_mem_smul_finset_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t := by
rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff ha, mem_coe]
#align finset.zero_mem_smul_finset_iff Finset.zero_mem_smul_finset_iff

end SMulZeroClass

section SMulWithZero

variable [Zero α] [Zero β] [SMulWithZero α β] [DecidableEq β] {s : Finset α} {t : Finset β}

/-!
Note that we have neither `SMulWithZero α (Finset β)` nor `SMulWithZero (Finset α) (Finset β)`
because `0 * ∅ ≠ 0`.
-/

lemma smul_zero_subset (s : Finset α) : s • (0 : Finset β) ⊆ 0 := by simp [subset_iff, mem_smul]
#align finset.smul_zero_subset Finset.smul_zero_subset

lemma zero_smul_subset (t : Finset β) : (0 : Finset α) • t ⊆ 0 := by simp [subset_iff, mem_smul]
#align finset.zero_smul_subset Finset.zero_smul_subset

lemma Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Finset β) = 0 :=
s.smul_zero_subset.antisymm $ by simpa [mem_smul] using hs
#align finset.nonempty.smul_zero Finset.Nonempty.smul_zero

lemma Nonempty.zero_smul (ht : t.Nonempty) : (0 : Finset α) • t = 0 :=
t.zero_smul_subset.antisymm $ by simpa [mem_smul] using ht
#align finset.nonempty.zero_smul Finset.Nonempty.zero_smul
Expand All @@ -2115,21 +2132,13 @@ lemma zero_smul_finset_subset (s : Finset β) : (0 : α) • s ⊆ 0 :=
image_subset_iff.2 fun x _ ↦ mem_zero.2 $ zero_smul α x
#align finset.zero_smul_finset_subset Finset.zero_smul_finset_subset

lemma zero_mem_smul_finset {t : Finset β} {a : α} (h : (0 : β) ∈ t) : (0 : β) ∈ a • t :=
mem_smul_finset.2 ⟨0, h, smul_zero _⟩
#align finset.zero_mem_smul_finset Finset.zero_mem_smul_finset

variable [NoZeroSMulDivisors α β] {a : α}

lemma zero_mem_smul_iff :
(0 : β) ∈ s • t ↔ (0 : α) ∈ s ∧ t.Nonempty ∨ (0 : β) ∈ t ∧ s.Nonempty := by
rw [← mem_coe, coe_smul, Set.zero_mem_smul_iff]; rfl
#align finset.zero_mem_smul_iff Finset.zero_mem_smul_iff

lemma zero_mem_smul_finset_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t := by
rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff ha, mem_coe]
#align finset.zero_mem_smul_finset_iff Finset.zero_mem_smul_finset_iff

end SMulWithZero

section GroupWithZero
Expand Down
43 changes: 25 additions & 18 deletions Mathlib/Data/Set/Pointwise/SMul.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -789,6 +789,31 @@ theorem op_smul_set_smul_eq_smul_smul_set (a : α) (s : Set β) (t : Set γ)

end SMul

section SMulZeroClass

variable [Zero β] [SMulZeroClass α β] {s : Set α} {t : Set β}

theorem smul_zero_subset (s : Set α) : s • (0 : Set β) ⊆ 0 := by simp [subset_def, mem_smul]
#align set.smul_zero_subset Set.smul_zero_subset

theorem Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Set β) = 0 :=
s.smul_zero_subset.antisymm <| by simpa [mem_smul] using hs
#align set.nonempty.smul_zero Set.Nonempty.smul_zero

theorem zero_mem_smul_set {a : α} (h : (0 : β) ∈ t) : (0 : β) ∈ a • t :=
⟨0, h, smul_zero _⟩
#align set.zero_mem_smul_set Set.zero_mem_smul_set

variable [Zero α] [NoZeroSMulDivisors α β] {a : α}
urkud marked this conversation as resolved.
Show resolved Hide resolved

theorem zero_mem_smul_set_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t := by
refine' ⟨_, zero_mem_smul_set⟩
rintro ⟨b, hb, h⟩
rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb
#align set.zero_mem_smul_set_iff Set.zero_mem_smul_set_iff

end SMulZeroClass

section SMulWithZero

variable [Zero α] [Zero β] [SMulWithZero α β] {s : Set α} {t : Set β}
Expand All @@ -798,17 +823,9 @@ Note that we have neither `SMulWithZero α (Set β)` nor `SMulWithZero (Set α)
because `0 * ∅ ≠ 0`.
-/


theorem smul_zero_subset (s : Set α) : s • (0 : Set β) ⊆ 0 := by simp [subset_def, mem_smul]
#align set.smul_zero_subset Set.smul_zero_subset

theorem zero_smul_subset (t : Set β) : (0 : Set α) • t ⊆ 0 := by simp [subset_def, mem_smul]
#align set.zero_smul_subset Set.zero_smul_subset

theorem Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Set β) = 0 :=
s.smul_zero_subset.antisymm <| by simpa [mem_smul] using hs
#align set.nonempty.smul_zero Set.Nonempty.smul_zero

theorem Nonempty.zero_smul (ht : t.Nonempty) : (0 : Set α) • t = 0 :=
t.zero_smul_subset.antisymm <| by simpa [mem_smul] using ht
#align set.nonempty.zero_smul Set.Nonempty.zero_smul
Expand All @@ -826,10 +843,6 @@ theorem subsingleton_zero_smul_set (s : Set β) : ((0 : α) • s).Subsingleton
subsingleton_singleton.anti <| zero_smul_set_subset s
#align set.subsingleton_zero_smul_set Set.subsingleton_zero_smul_set

theorem zero_mem_smul_set {t : Set β} {a : α} (h : (0 : β) ∈ t) : (0 : β) ∈ a • t :=
⟨0, h, smul_zero _⟩
#align set.zero_mem_smul_set Set.zero_mem_smul_set

variable [NoZeroSMulDivisors α β] {a : α}

theorem zero_mem_smul_iff :
Expand All @@ -844,12 +857,6 @@ theorem zero_mem_smul_iff :
· exact ⟨a, 0, ha, ht, smul_zero _⟩
#align set.zero_mem_smul_iff Set.zero_mem_smul_iff

theorem zero_mem_smul_set_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t := by
refine' ⟨_, zero_mem_smul_set⟩
rintro ⟨b, hb, h⟩
rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb
#align set.zero_mem_smul_set_iff Set.zero_mem_smul_set_iff

end SMulWithZero

section Semigroup
Expand Down