[Merged by Bors] - feat(linear_algebra/finite_dimension): nontriviality lemmas

src/analysis/normed_space/inner_product.lean

@@ -2637,7 +2637,7 @@ lemma submodule.finrank_add_finrank_orthogonal' [finite_dimensional 𝕜 E] {K :
   finrank 𝕜 Kᗮ = n :=
 by { rw ← add_right_inj (finrank 𝕜 K), simp [submodule.finrank_add_finrank_orthogonal, h_dim] }
 
-local attribute [instance] finite_dimensional_of_finrank_eq_succ
+local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ
 
 /-- In a finite-dimensional inner product space, the dimension of the orthogonal complement of the
 span of a nonzero vector is one less than the dimension of the space. -/

src/analysis/normed_space/pi_Lp.lean

@@ -457,7 +457,7 @@ def linear_isometry_equiv.of_inner_product_space
   E ≃ₗᵢ[𝕜] (euclidean_space 𝕜 (fin n)) :=
 (fin_orthonormal_basis hn).isometry_euclidean_of_orthonormal (fin_orthonormal_basis_orthonormal hn)
 
-local attribute [instance] finite_dimensional_of_finrank_eq_succ
+local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ
 
 /-- Given a natural number `n` one less than the `finrank` of a finite-dimensional inner product
 space, there exists an isometry from the orthogonal complement of a nonzero singleton to

src/geometry/manifold/instances/sphere.lean

@@ -58,7 +58,7 @@ noncomputable theory
 open metric finite_dimensional
 open_locale manifold
 
-local attribute [instance] finite_dimensional_of_finrank_eq_succ
+local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ
 
 section stereographic_projection
 variables (v : E)

src/linear_algebra/finite_dimensional.lean

@@ -161,9 +161,13 @@ lemma finite_dimensional_of_finrank {K V : Type*} [field K] [add_comm_group V] [
   (h : 0 < finrank K V) : finite_dimensional K V :=
 by { contrapose h, simp [finrank_of_infinite_dimensional h] }
 
+lemma finite_dimensional_of_finrank_eq_succ {K V : Type*} [field K] [add_comm_group V] [module K V]
+  {n : ℕ} (hn : finrank K V = n.succ) : finite_dimensional K V :=
+finite_dimensional_of_finrank $ by rw hn; exact n.succ_pos
+
 /-- We can infer `finite_dimensional K V` in the presence of `[fact (finrank K V = n + 1)]`. Declare
 this as a local instance where needed. -/
-lemma finite_dimensional_of_finrank_eq_succ {K V : Type*} [field K] [add_comm_group V]
+lemma fact_finite_dimensional_of_finrank_eq_succ {K V : Type*} [field K] [add_comm_group V]
   [module K V] (n : ℕ) [fact (finrank K V = n + 1)] :
   finite_dimensional K V :=
 finite_dimensional_of_finrank $ by convert nat.succ_pos n; apply fact.out
@@ -303,6 +307,18 @@ iff.trans (by { rw ← finrank_eq_dim, norm_cast }) (@dim_pos_iff_exists_ne_zero
 lemma finrank_pos_iff [finite_dimensional K V] : 0 < finrank K V ↔ nontrivial V :=
 iff.trans (by { rw ← finrank_eq_dim, norm_cast }) (@dim_pos_iff_nontrivial K V _ _ _)
 
+/-- A finite dimensional space is nontrivial if it has positive `finrank`. -/
+lemma nontrivial_of_finrank_pos (h : 0 < finrank K V) : nontrivial V :=
+begin
+  haveI : finite_dimensional K V := finite_dimensional_of_finrank h,
+  rwa finrank_pos_iff at h
+end
+
+/-- A finite dimensional space is nontrivial if it has `finrank` equal to the successor of a
+natural number. -/
+lemma nontrivial_of_finrank_eq_succ {n : ℕ} (hn : finrank K V = n.succ) : nontrivial V :=
+nontrivial_of_finrank_pos (by rw hn; exact n.succ_pos)
+
 /-- A nontrivial finite dimensional space has positive `finrank`. -/
 lemma finrank_pos [finite_dimensional K V] [h : nontrivial V] : 0 < finrank K V :=
 finrank_pos_iff.mpr h