feat(linear_algebra/basic): add span_zero (#3306)

`simp` now proves span_zero for both submodules and ideals



Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/linear_algebra/basic.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
 import algebra.pi_instances
 import data.finsupp
+import algebra.pointwise
 
 /-!
 # Linear algebra
@@ -806,9 +807,11 @@ eq_bot_iff.trans ⟨
   λ H x h, (mem_bot R).1 $ H $ subset_span h,
   λ H, span_le.2 (λ x h, (mem_bot R).2 $ H x h)⟩
 
-lemma span_singleton_eq_bot : span R ({x} : set M) = ⊥ ↔ x = 0 :=
+@[simp] lemma span_singleton_eq_bot : span R ({x} : set M) = ⊥ ↔ x = 0 :=
 span_eq_bot.trans $ by simp
 
+@[simp] lemma span_zero : span R (0 : set M) = ⊥ := by rw [←singleton_zero, span_singleton_eq_bot]
+
 @[simp] lemma span_image (f : M →ₗ[R] M₂) : span R (f '' s) = map f (span R s) :=
 span_eq_of_le _ (image_subset _ subset_span) $ map_le_iff_le_comap.2 $
 span_le.2 $ image_subset_iff.1 subset_span

src/linear_algebra/basis.lean

@@ -880,7 +880,7 @@ begin
     intro hi,
     simp [hi] },
   { refine top_unique (λ _ _, _),
-    simp [submodule.mem_span_singleton] }
+    simp only [mem_span_singleton, range_const, mul_one, exists_eq, smul_eq_mul] }
 end
 
 protected lemma linear_equiv.is_basis (hs : is_basis R v)

src/ring_theory/fractional_ideal.lean

@@ -562,7 +562,7 @@ lemma is_principal_iff (I : fractional_ideal f) :
 by { ext, simp [submodule.mem_span_singleton, eq_comm, -singleton_zero] }
 
 lemma span_singleton_eq_zero_iff {y : f.codomain} : span_singleton y = 0 ↔ y = 0 :=
-⟨ λ h, span_eq_bot.mp (by simpa using congr_arg subtype.val h) y (mem_singleton y),
+⟨ λ h, span_eq_bot.mp (by simpa using congr_arg subtype.val h : span R {y} = ⊥) y (mem_singleton y),
   λ h, by simp [h] ⟩
 
 @[simp] lemma span_singleton_one : span_singleton (1 : f.codomain) = 1 :=

src/ring_theory/ideals.lean

@@ -70,7 +70,10 @@ span_le.trans $ singleton_subset_iff.trans mem_span_singleton
 
 lemma span_eq_bot {s : set α} : span s = ⊥ ↔ ∀ x ∈ s, (x:α) = 0 := submodule.span_eq_bot
 
-lemma span_singleton_eq_bot {x} : span ({x} : set α) = ⊥ ↔ x = 0 := submodule.span_singleton_eq_bot
+@[simp] lemma span_singleton_eq_bot {x} : span ({x} : set α) = ⊥ ↔ x = 0 :=
+submodule.span_singleton_eq_bot
+
+@[simp] lemma span_zero : span (0 : set α) = ⊥ := by rw [←set.singleton_zero, span_singleton_eq_bot]
 
 lemma span_singleton_eq_top {x} : span ({x} : set α) = ⊤ ↔ is_unit x :=
 by rw [is_unit_iff_dvd_one, ← span_singleton_le_span_singleton, singleton_one, span_singleton_one,
@@ -139,7 +142,8 @@ theorem is_maximal.is_prime {I : ideal α} (H : I.is_maximal) : I.is_prime :=
 end⟩
 
 @[priority 100] -- see Note [lower instance priority]
-instance is_maximal.is_prime' (I : ideal α) : ∀ [H : I.is_maximal], I.is_prime := is_maximal.is_prime
+instance is_maximal.is_prime' (I : ideal α) : ∀ [H : I.is_maximal], I.is_prime :=
+is_maximal.is_prime
 
 theorem exists_le_maximal (I : ideal α) (hI : I ≠ ⊤) :
   ∃ M : ideal α, M.is_maximal ∧ I ≤ M :=