Loogle!

Result

Found 1323 declarations mentioning FiniteDimensional. Of these, only the first 200 are shown.

• FiniteDimensional 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Prop
• FiniteDimensional.finiteDimensional_self 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) [DivisionRing K] : FiniteDimensional K K
• FiniteDimensional.instFintypeElemOfVectorSpaceIndex 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Fintype ↑(Basis.ofVectorSpaceIndex K V)
• FiniteDimensional.fintypeBasisIndex 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [FiniteDimensional K V] (b : Basis ι K V) : Fintype ι
• FiniteDimensional.of_fintype_basis 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} [Finite ι] (h : Basis ι K V) : FiniteDimensional K V
• FiniteDimensional.of_finrank_eq_succ 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (hn : Module.finrank K V = n.succ) : FiniteDimensional K V
• FiniteDimensional.of_finrank_pos 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : 0 < Module.finrank K V) : FiniteDimensional K V
• Module.finrank_of_infinite_dimensional 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : ¬FiniteDimensional K V) : Module.finrank K V = 0
• FiniteDimensional.of_finite_basis 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} {s : Set ι} (h : Basis (↑s) K V) (hs : s.Finite) : FiniteDimensional K V
• FiniteDimensional.finiteDimensional_pi 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] : FiniteDimensional K (ι → K)
• FiniteDimensional.of_fact_finrank_eq_succ 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (n : ℕ) [hn : Fact (Module.finrank K V = n + 1)] : FiniteDimensional K V
• Module.finrank_eq_rank' 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : ↑(Module.finrank K V) = Module.rank K V
• Module.finrank_eq_card_basis' 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type w} (h : Basis ι K V) : ↑(Module.finrank K V) = Cardinal.mk ι
• FiniteDimensional.finiteDimensional_pi' 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] (M : ι → Type u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module K (M i)] [∀ (i : ι), FiniteDimensional K (M i)] : FiniteDimensional K ((i : ι) → M i)
• FiniteDimensional.finiteDimensional_quotient 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K (V ⧸ S)
• LinearEquiv.finiteDimensional 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V ≃ₗ[K] V₂) [FiniteDimensional K V] : FiniteDimensional K V₂
• Module.finiteDimensional_iff_of_rank_eq_nsmul 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {W : Type v} [AddCommGroup W] [Module K W] {n : ℕ} (hn : n ≠ 0) (hVW : Module.rank K V = n • Module.rank K W) : FiniteDimensional K V ↔ FiniteDimensional K W
• FiniteDimensional.finiteDimensional_submodule 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Submodule K V) : FiniteDimensional K ↥S
• Submodule.fg_iff_finiteDimensional 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) : s.FG ↔ FiniteDimensional K ↥s
• FiniteDimensional.span_of_finite 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {A : Set V} (hA : A.Finite) : FiniteDimensional K ↥(Submodule.span K A)
• FiniteDimensional.span_finset 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Finset V) : FiniteDimensional K ↥(Submodule.span K ↑s)
• FiniteDimensional.span_singleton 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (x : V) : FiniteDimensional K ↥(Submodule.span K {x})
• FiniteDimensional.of_injective 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (w : Function.Injective ⇑f) [FiniteDimensional K V₂] : FiniteDimensional K V
• FiniteDimensional.of_surjective 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (w : Function.Surjective ⇑f) [FiniteDimensional K V] : FiniteDimensional K V₂
• FiniteDimensional.trans 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (F : Type u_1) (K : Type u_2) (A : Type u_3) [DivisionRing F] [DivisionRing K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [FiniteDimensional F K] [FiniteDimensional K A] : FiniteDimensional F A
• FiniteDimensional.instSubtypeMemSubmoduleMapLinearMapId 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) [FiniteDimensional K ↥p] : FiniteDimensional K ↥(Submodule.map f p)
• FiniteDimensional.of_rank_eq_nat 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (h : Module.rank K V = ↑n) : FiniteDimensional K V
• FiniteDimensional.of_rank_eq_one 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V = 1) : FiniteDimensional K V
• FiniteDimensional.of_rank_eq_zero 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V = 0) : FiniteDimensional K V
• divisionRingOfFiniteDimensional 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  (F : Type u_1) (K : Type u_2) [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] : DivisionRing K
• LinearIndependent.lt_aleph0_of_finiteDimensional 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} [FiniteDimensional K V] {v : ι → V} (h : LinearIndependent K v) : Cardinal.mk ι < Cardinal.aleph0
• fieldOfFiniteDimensional 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  (F : Type u_1) (K : Type u_2) [Field F] [h : CommRing K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] : Field K
• basisOfFinrankZero 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} [IsEmpty ι] (hV : Module.finrank K V = 0) : Basis ι K V
• finiteDimensional_finsupp 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Finite ι] [FiniteDimensional K V] : FiniteDimensional K (ι →₀ V)
• finrank_zero_iff_forall_zero 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Module.finrank K V = 0 ↔ ∀ (x : V), x = 0
• Set.finrank_mono 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s t : Set V} (h : s ⊆ t) : Set.finrank K s ≤ Set.finrank K t
• FiniteDimensional.isUnit 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  (F : Type u_1) {K : Type u_2} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : IsUnit x
• FiniteDimensional.exists_mul_eq_one 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  (F : Type u_1) {K : Type u_2} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : ∃ y, x * y = 1
• finiteDimensional_bot 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] : FiniteDimensional K ↥⊥
• Submodule.eq_top_of_finrank_eq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {S : Submodule K V} (h : Module.finrank K ↥S = Module.finrank K V) : S = ⊤
• FiniteDimensional.finiteDimensional_subalgebra 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] [FiniteDimensional F E] (S : Subalgebra F E) : FiniteDimensional F ↥S
• LinearEquiv.ofInjectiveEndo 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f) : V ≃ₗ[K] V
• LinearMap.surjective_of_injective 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} (hinj : Function.Injective ⇑f) : Function.Surjective ⇑f
• LinearMap.injective_iff_surjective 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} : Function.Injective ⇑f ↔ Function.Surjective ⇑f
• LinearMap.finiteDimensional_of_surjective 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) (hf : LinearMap.range f = ⊤) : FiniteDimensional K V₂
• Submodule.finiteDimensional_inf_left 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ S₂ : Submodule K V) [FiniteDimensional K ↥S₁] : FiniteDimensional K ↥(S₁ ⊓ S₂)
• Submodule.finiteDimensional_inf_right 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ S₂ : Submodule K V) [FiniteDimensional K ↥S₂] : FiniteDimensional K ↥(S₁ ⊓ S₂)
• Submodule.finiteDimensional_of_le 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂] (h : S₁ ≤ S₂) : FiniteDimensional K ↥S₁
• LinearMap.isUnit_iff_ker_eq_bot 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ LinearMap.ker f = ⊥
• LinearMap.isUnit_iff_range_eq_top 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ LinearMap.range f = ⊤
• FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {L : Type u_1} [Field L] [LinearOrder L] [IsStrictOrderedRing L] {W : Type v} [AddCommGroup W] [Module L W] [FiniteDimensional L W] {t : Finset W} (h : Module.finrank L W + 1 < t.card) : ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x
• Submodule.finiteDimensional_iSup 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Sort u_1} [Finite ι] (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K ↥(S i)] : FiniteDimensional K ↥(⨆ i, S i)
• LinearMap.comp_eq_id_comm 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f g : V →ₗ[K] V} : f ∘ₗ g = LinearMap.id ↔ g ∘ₗ f = LinearMap.id
• Submodule.eq_of_le_of_finrank_eq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂] (hle : S₁ ≤ S₂) (hd : Module.finrank K ↥S₁ = Module.finrank K ↥S₂) : S₁ = S₂
• Submodule.eq_of_le_of_finrank_le 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂] (hle : S₁ ≤ S₂) (hd : Module.finrank K ↥S₂ ≤ Module.finrank K ↥S₁) : S₁ = S₂
• LinearEquiv.coe_ofInjectiveEndo 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f) : ⇑(LinearEquiv.ofInjectiveEndo f h_inj) = ⇑f
• LinearMap.ker_eq_bot_iff_range_eq_top 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : V →ₗ[K] V} : LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤
• Submodule.finiteDimensional_finset_sup 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} (s : Finset ι) (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K ↥(S i)] : FiniteDimensional K ↥(s.sup S)
• Submodule.finiteDimensional_sup 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (S₁ S₂ : Submodule K V) [h₁ : FiniteDimensional K ↥S₁] [h₂ : FiniteDimensional K ↥S₂] : FiniteDimensional K ↥(S₁ ⊔ S₂)
• LinearEquiv.ofInjectiveEndo_left_inv 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f) : ↑(LinearEquiv.ofInjectiveEndo f h_inj).symm * f = 1
• LinearEquiv.ofInjectiveEndo_right_inv 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f) : f * ↑(LinearEquiv.ofInjectiveEndo f h_inj).symm = 1
• LinearMap.injOn_iff_surjOn 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {p : Submodule K V} [FiniteDimensional K ↥p] {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) : Set.InjOn ⇑f ↑p ↔ Set.SurjOn ⇑f ↑p ↑p
• LinearMap.finiteDimensional_range 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) : FiniteDimensional K ↥(LinearMap.range f)
• LinearMap.mul_eq_one_of_mul_eq_one 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f g : V →ₗ[K] V} (hfg : f * g = 1) : g * f = 1
• LinearMap.mul_eq_one_comm 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f g : V →ₗ[K] V} : f * g = 1 ↔ g * f = 1
• Subalgebra.eq_of_le_of_finrank_eq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u_1} {L : Type u_2} [Field K] [Ring L] [Algebra K L] {F E : Subalgebra K L} [hfin : FiniteDimensional K ↥E] (h_le : F ≤ E) (h_finrank : Module.finrank K ↥F = Module.finrank K ↥E) : F = E
• Subalgebra.eq_of_le_of_finrank_le 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u_1} {L : Type u_2} [Field K] [Ring L] [Algebra K L] {F E : Subalgebra K L} [hfin : FiniteDimensional K ↥E] (h_le : F ≤ E) (h_finrank : Module.finrank K ↥E ≤ Module.finrank K ↥F) : F = E
• LinearMap.comap_eq_sup_ker_of_disjoint 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {p : Submodule K V} [FiniteDimensional K ↥p] {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) (h' : Disjoint p (LinearMap.ker f)) : Submodule.comap f p = p ⊔ LinearMap.ker f
• LinearMap.ker_noncommProd_eq_of_supIndep_ker 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} {f : ι → V →ₗ[K] V} (s : Finset ι) (comm : (↑s).Pairwise (Function.onFun Commute f)) (h : s.SupIndep fun i => LinearMap.ker (f i)) : LinearMap.ker (s.noncommProd f comm) = ⨆ i ∈ s, LinearMap.ker (f i)
• LinearMap.ker_comp_eq_of_commute_of_disjoint_ker 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f g : V →ₗ[K] V} (h : Commute f g) (h' : Disjoint (LinearMap.ker f) (LinearMap.ker g)) : LinearMap.ker (f ∘ₗ g) = LinearMap.ker f ⊔ LinearMap.ker g
• FiniteDimensional.of_subalgebra_toSubmodule 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F ↥(Subalgebra.toSubmodule S) → FiniteDimensional F ↥S
• FiniteDimensional.subalgebra_toSubmodule 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F ↥S → FiniteDimensional F ↥(Subalgebra.toSubmodule S)
• Subalgebra.finiteDimensional_toSubmodule 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {F : Type u_1} {E : Type u_2} [Field F] [Ring E] [Algebra F E] {S : Subalgebra F E} : FiniteDimensional F ↥(Subalgebra.toSubmodule S) ↔ FiniteDimensional F ↥S
• CSA.fin_dim 📋 Mathlib.Algebra.BrauerGroup.Defs
  {K : Type u} [Field K] (self : CSA K) : FiniteDimensional K ↑self.toAlgebraCat
• CSA.mk 📋 Mathlib.Algebra.BrauerGroup.Defs
  {K : Type u} [Field K] (toAlgebraCat : AlgebraCat K) [isCentral : Algebra.IsCentral K ↑toAlgebraCat] [isSimple : IsSimpleRing ↑toAlgebraCat] [fin_dim : FiniteDimensional K ↑toAlgebraCat] : CSA K
• CSA.mk.injEq 📋 Mathlib.Algebra.BrauerGroup.Defs
  {K : Type u} [Field K] (toAlgebraCat : AlgebraCat K) [isCentral : Algebra.IsCentral K ↑toAlgebraCat] [isSimple : IsSimpleRing ↑toAlgebraCat] [fin_dim : FiniteDimensional K ↑toAlgebraCat] (toAlgebraCat✝ : AlgebraCat K) (isCentral✝ : Algebra.IsCentral K ↑toAlgebraCat✝) (isSimple✝ : IsSimpleRing ↑toAlgebraCat✝) (fin_dim✝ : FiniteDimensional K ↑toAlgebraCat✝) : ({ toAlgebraCat := toAlgebraCat, isCentral := isCentral, isSimple := isSimple, fin_dim := fin_dim } = { toAlgebraCat := toAlgebraCat✝, isCentral := isCentral✝, isSimple := isSimple✝, fin_dim := fin_dim✝ }) = (toAlgebraCat = toAlgebraCat✝)
• CSA.mk.sizeOf_spec 📋 Mathlib.Algebra.BrauerGroup.Defs
  {K : Type u} [Field K] [SizeOf K] (toAlgebraCat : AlgebraCat K) [isCentral : Algebra.IsCentral K ↑toAlgebraCat] [isSimple : IsSimpleRing ↑toAlgebraCat] [fin_dim : FiniteDimensional K ↑toAlgebraCat] : sizeOf { toAlgebraCat := toAlgebraCat, isCentral := isCentral, isSimple := isSimple, fin_dim := fin_dim } = 1 + sizeOf toAlgebraCat + sizeOf isCentral + sizeOf isSimple + sizeOf fin_dim
• LinearIndependent.span_eq_top_of_card_eq_finrank' 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Fintype ι] [FiniteDimensional K V] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) : Submodule.span K (Set.range b) = ⊤
• Submodule.finrank_lt 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s : Submodule K V} (h : s ≠ ⊤) : Module.finrank K ↥s < Module.finrank K V
• Submodule.finrank_strictMono 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : StrictMono fun s => Module.finrank K ↥s
• LinearMap.linearEquivOfInjective 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (f : V →ₗ[K] V₂) (hf : Function.Injective ⇑f) (hdim : Module.finrank K V = Module.finrank K V₂) : V ≃ₗ[K] V₂
• LinearMap.injective_iff_surjective_of_finrank_eq_finrank 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (H : Module.finrank K V = Module.finrank K V₂) {f : V →ₗ[K] V₂} : Function.Injective ⇑f ↔ Function.Surjective ⇑f
• LinearMap.ker_ne_bot_of_finrank_lt 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (h : Module.finrank K V₂ < Module.finrank K V) : LinearMap.ker f ≠ ⊥
• Submodule.finrank_add_finrank_le_of_disjoint 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s t : Submodule K V} (hdisjoint : Disjoint s t) : Module.finrank K ↥s + Module.finrank K ↥t ≤ Module.finrank K V
• Submodule.finrank_add_eq_of_isCompl 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (h : IsCompl U W) : Module.finrank K ↥U + Module.finrank K ↥W = Module.finrank K V
• Submodule.finrank_lt_finrank_of_lt 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Submodule K V} [FiniteDimensional K ↥t] (hst : s < t) : Module.finrank K ↥s < Module.finrank K ↥t
• FiniteDimensional.LinearEquiv.quotEquivOfQuotEquiv 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {p q : Subspace K V} (f : (V ⧸ p) ≃ₗ[K] ↥q) : (V ⧸ q) ≃ₗ[K] ↥p
• Submodule.isCompl_iff_disjoint 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (s t : Submodule K V) (hdim : Module.finrank K V ≤ Module.finrank K ↥s + Module.finrank K ↥t) : IsCompl s t ↔ Disjoint s t
• Submodule.eq_top_of_disjoint 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (s t : Submodule K V) (hdim : Module.finrank K V ≤ Module.finrank K ↥s + Module.finrank K ↥t) (hdisjoint : Disjoint s t) : s ⊔ t = ⊤
• Module.End.exists_ker_pow_eq_ker_pow_succ 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : ∃ k ≤ Module.finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
• FiniteDimensional.LinearEquiv.quotEquivOfEquiv 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {p : Subspace K V} {q : Subspace K V₂} (f₁ : ↥p ≃ₗ[K] ↥q) (f₂ : V ≃ₗ[K] V₂) : (V ⧸ p) ≃ₗ[K] V₂ ⧸ q
• Module.End.ker_pow_eq_ker_pow_finrank_of_le 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {m : ℕ} (hm : Module.finrank K V ≤ m) : LinearMap.ker (f ^ m) = LinearMap.ker (f ^ Module.finrank K V)
• LinearMap.linearEquivOfInjective_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂} (hf : Function.Injective ⇑f) (hdim : Module.finrank K V = Module.finrank K V₂) (x : V) : (f.linearEquivOfInjective hf hdim) x = f x
• LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] [FiniteDimensional K V₂] (H : Module.finrank K V = Module.finrank K V₂) {f : V →ₗ[K] V₂} : LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤
• Module.End.ker_pow_le_ker_pow_finrank 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (m : ℕ) : LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ Module.finrank K V)
• Submodule.finrank_add_le_finrank_add_finrank 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s t : Submodule K V) [FiniteDimensional K ↥s] [FiniteDimensional K ↥t] : Module.finrank K ↥(s ⊔ t) ≤ Module.finrank K ↥s + Module.finrank K ↥t
• Submodule.finrank_sup_add_finrank_inf_eq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s t : Submodule K V) [FiniteDimensional K ↥s] [FiniteDimensional K ↥t] : Module.finrank K ↥(s ⊔ t) + Module.finrank K ↥(s ⊓ t) = Module.finrank K ↥s + Module.finrank K ↥t
• LinearMap.finrank_range_add_finrank_ker 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂] [Module K V₂] [FiniteDimensional K V] (f : V →ₗ[K] V₂) : Module.finrank K ↥(LinearMap.range f) + Module.finrank K ↥(LinearMap.ker f) = Module.finrank K V
• FiniteDimensional.eq_1 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : FiniteDimensional K V = Module.Finite K V
• Module.instFiniteDimensionalOfIsReflexive 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  (K : Type u_4) (V : Type u_5) [Field K] [AddCommGroup V] [Module K V] [Module.IsReflexive K V] : FiniteDimensional K V
• Subspace.instModuleDualFiniteDimensional 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : FiniteDimensional K (Module.Dual K V)
• Basis.linearEquiv_dual_iff_finiteDimensional 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type uK} {V : Type uV} [Field K] [AddCommGroup V] [Module K V] : Nonempty (V ≃ₗ[K] Module.Dual K V) ↔ FiniteDimensional K V
• Module.Dual.eq_of_ker_eq_of_apply_eq 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] [FiniteDimensional K V₁] {f g : Module.Dual K V₁} (x : V₁) (h : LinearMap.ker f = LinearMap.ker g) (h' : f x = g x) (hx : f x ≠ 0) : f = g
• Module.Dual.isCompl_ker_of_disjoint_of_ne_bot 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] {f : Module.Dual K V₁} (hf : f ≠ 0) [FiniteDimensional K V₁] {p : Submodule K V₁} (hpf : Disjoint (LinearMap.ker f) p) (hp : p ≠ ⊥) : IsCompl (LinearMap.ker f) p
• Module.Dual.finrank_ker_add_one_of_ne_zero 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] {f : Module.Dual K V₁} (hf : f ≠ 0) [FiniteDimensional K V₁] : Module.finrank K ↥(LinearMap.ker f) + 1 = Module.finrank K V₁
• Subspace.finrank_add_finrank_dualAnnihilator_eq 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) : Module.finrank K ↥W + Module.finrank K ↥(Submodule.dualAnnihilator W) = Module.finrank K V
• Subspace.quotEquivAnnihilator 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) : (V ⧸ W) ≃ₗ[K] ↥(Submodule.dualAnnihilator W)
• Subspace.finiteDimensional_quot_dualCoannihilator_iff 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {W : Submodule K (Module.Dual K V)} : FiniteDimensional K (V ⧸ W.dualCoannihilator) ↔ FiniteDimensional K ↥W
• Subspace.finrank_add_finrank_dualCoannihilator_eq 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K (Module.Dual K V)) : Module.finrank K ↥W + Module.finrank K ↥(Submodule.dualCoannihilator W) = Module.finrank K V
• Subspace.dualCoannihilator_dualAnnihilator_eq 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {W : Subspace K (Module.Dual K V)} [FiniteDimensional K ↥W] : (Submodule.dualCoannihilator W).dualAnnihilator = W
• Subspace.orderIsoFiniteDimensional 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] : Subspace K V ≃o (Subspace K (Module.Dual K V))ᵒᵈ
• FiniteDimensional.mem_span_of_iInf_ker_le_ker 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {ι : Type u_3} {𝕜 : Type u_4} {E : Type u_5} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] {L : ι → E →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜} (h : ⨅ i, LinearMap.ker (L i) ≤ LinearMap.ker K) : K ∈ Submodule.span 𝕜 (Set.range L)
• LinearMap.flip_bijective_iff₁ 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Bijective ⇑B.flip ↔ Function.Bijective ⇑B
• LinearMap.flip_bijective_iff₂ 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Bijective ⇑B.flip ↔ Function.Bijective ⇑B
• LinearMap.flip_injective_iff₁ 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Injective ⇑B.flip ↔ Function.Surjective ⇑B
• LinearMap.flip_injective_iff₂ 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Injective ⇑B.flip ↔ Function.Surjective ⇑B
• LinearMap.flip_surjective_iff₁ 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁] : Function.Surjective ⇑B.flip ↔ Function.Injective ⇑B
• LinearMap.flip_surjective_iff₂ 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [Field K] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂] : Function.Surjective ⇑B.flip ↔ Function.Injective ⇑B
• Subspace.dualAnnihilator_dualAnnihilator_eq_map 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) [FiniteDimensional K ↥W] : (Submodule.dualAnnihilator W).dualAnnihilator = Submodule.map (Module.Dual.eval K V) W
• Subspace.map_dualCoannihilator 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K (Module.Dual K V)) [FiniteDimensional K V] : Submodule.map (Module.Dual.eval K V) (Submodule.dualCoannihilator W) = Submodule.dualAnnihilator W
• Subspace.orderIsoFiniteCodimDim 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] : { W // FiniteDimensional K (V ⧸ W) } ≃o { W // FiniteDimensional K ↥W }ᵒᵈ
• Subspace.finrank_dualCoannihilator_eq 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Φ : Subspace K (Module.Dual K V)} : Module.finrank K ↥(Submodule.dualCoannihilator Φ) = Module.finrank K ↥(Submodule.dualAnnihilator Φ)
• Subspace.flip_quotDualCoannihilatorToDual_bijective 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K (Module.Dual K V)) [FiniteDimensional K ↥W] : Function.Bijective ⇑(Submodule.quotDualCoannihilatorToDual W).flip
• Subspace.dualQuotDistrib 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} [Field K] [AddCommGroup V₁] [Module K V₁] [FiniteDimensional K V₁] (W : Subspace K V₁) : Module.Dual K (V₁ ⧸ W) ≃ₗ[K] Module.Dual K V₁ ⧸ LinearMap.range W.dualLift
• Subspace.dualAnnihilator_dualAnnihilator_eq 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) : (Submodule.dualAnnihilator W).dualAnnihilator = (Module.mapEvalEquiv K V) W
• Subspace.quotDualEquivAnnihilator 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (W : Subspace K V) : (Module.Dual K V ⧸ LinearMap.range W.dualLift) ≃ₗ[K] ↥(Submodule.dualAnnihilator W)
• Subspace.quotDualCoannihilatorToDual_bijective 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K (Module.Dual K V)) [FiniteDimensional K ↥W] : Function.Bijective ⇑(Submodule.quotDualCoannihilatorToDual W)
• coevaluation 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : K →ₗ[K] TensorProduct K V (Module.Dual K V)
• coevaluation_apply_one 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : (coevaluation K V) 1 = let bV := Basis.ofVectorSpace K V; ∑ i, bV i ⊗ₜ[K] bV.coord i
• coevaluation.eq_1 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : coevaluation K V = ((Basis.singleton Unit K).constr K) fun x => ∑ i, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i
• contractLeft_assoc_coevaluation' 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V) = ↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)
• contractLeft_assoc_coevaluation 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V) = ↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V))
• FGModuleCat.instFiniteDimensionalCarrierPiObjModuleCatOfFinite 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {k : Type v} [Field k] {J : Type} [Finite J] (Z : J → ModuleCat k) [∀ (j : J), FiniteDimensional k ↑(Z j)] : FiniteDimensional k ↑(∏ᶜ fun j => Z j)
• FGModuleCat.instFiniteDimensionalCarrierLimitModuleCatCompForget₂ 📋 Mathlib.Algebra.Category.FGModuleCat.Limits
  {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type v} [Field k] (F : CategoryTheory.Functor J (FGModuleCat k)) : FiniteDimensional k ↑(CategoryTheory.Limits.limit (F.comp (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))
• IsLocalRing.instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing 📋 Mathlib.RingTheory.Ideal.Cotangent
  (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : FiniteDimensional (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)
• LinearMap.BilinForm.exists_orthogonal_basis 📋 Mathlib.LinearAlgebra.QuadraticForm.Basic
  {V : Type u} {K : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [hK : Invertible 2] {B : LinearMap.BilinForm K V} (hB₂ : LinearMap.IsSymm B) : ∃ v, LinearMap.IsOrthoᵢ B ⇑v
• QuadraticForm.equivalent_weightedSumSquares 📋 Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
  {K : Type u_3} {V : Type u_8} [Field K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) : ∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K w)
• QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate' 📋 Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
  {K : Type u_3} {V : Type u_8} [Field K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) : ∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K w)
• AlgHom.bijective 📋 Mathlib.RingTheory.Algebraic.Integral
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ⇑ϕ
• algEquivEquivAlgHom 📋 Mathlib.RingTheory.Algebraic.Integral
  (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)
• IsIntegralClosure.isFractionRing_of_finite_extension 📋 Mathlib.RingTheory.Localization.Integral
  (A : Type u_3) (K : Type u_4) [CommRing A] (L : Type u_5) [Field K] [Field L] [Algebra A K] [Algebra A L] [IsFractionRing A K] (C : Type u_6) [CommRing C] [IsDomain C] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [IsDomain A] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] : IsFractionRing C L
• integralClosure.isFractionRing_of_finite_extension 📋 Mathlib.RingTheory.Localization.Integral
  {A : Type u_3} (K : Type u_4) [CommRing A] (L : Type u_5) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [IsDomain A] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] : IsFractionRing (↥(integralClosure A L)) L
• Module.End.maxUnifEigenspaceIndex_le_finrank 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) : f.maxUnifEigenspaceIndex μ ≤ Module.finrank K V
• Module.End.HasEigenvalue.of_mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : μ ∈ spectrum K f → f.HasEigenvalue μ
• Module.End.hasEigenvalue_iff_mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : f.HasEigenvalue μ ↔ μ ∈ spectrum K f
• Module.End.HasUnifEigenvalue.of_mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : μ ∈ spectrum K f → f.HasUnifEigenvalue μ 1
• Module.End.hasUnifEigenvalue_iff_mem_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f
• Module.End.maxGenEigenspace_eq_genEigenspace_finrank 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) : f.maxGenEigenspace μ = (f.genEigenspace μ) ↑(Module.finrank K V)
• Module.End.generalized_eigenvec_disjoint_range_ker 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) : Disjoint (f.genEigenrange μ ↑(Module.finrank K V)) ((f.genEigenspace μ) ↑(Module.finrank K V))
• Module.End.genEigenspace_eq_genEigenspace_finrank_of_le 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) {k : ℕ} (hk : Module.finrank K V ≤ k) : (f.genEigenspace μ) ↑k = (f.genEigenspace μ) ↑(Module.finrank K V)
• Module.End.genEigenspace_le_genEigenspace_finrank 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) (k : ℕ∞) : (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ↑(Module.finrank K V)
• Module.End.pos_finrank_genEigenspace_of_hasEigenvalue 📋 Mathlib.LinearAlgebra.Eigenspace.Basic
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {k : ℕ} {μ : K} (hx : f.HasEigenvalue μ) (hk : 0 < k) : 0 < Module.finrank K ↥((f.genEigenspace μ) ↑k)
• integralClosure.isIntegrallyClosedOfFiniteExtension 📋 Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
  {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {L : Type u_3} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsDomain R] [FiniteDimensional K L] : IsIntegrallyClosed ↥(integralClosure R L)
• LinearMap.finiteDimensional_of_det_ne_one 📋 Mathlib.LinearAlgebra.Determinant
  {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_7} [Field 𝕜] [Module 𝕜 M] (f : M →ₗ[𝕜] M) (hf : LinearMap.det f ≠ 1) : FiniteDimensional 𝕜 M
• LinearMap.equivOfDetNeZero 📋 Mathlib.LinearAlgebra.Determinant
  {𝕜 : Type u_5} [Field 𝕜] {M : Type u_6} [AddCommGroup M] [Module 𝕜 M] [FiniteDimensional 𝕜 M] (f : M →ₗ[𝕜] M) (hf : LinearMap.det f ≠ 0) : M ≃ₗ[𝕜] M
• minpoly.AlgHom.fintype 📋 Mathlib.FieldTheory.Minpoly.Field
  (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Ring E] [CommRing K] [IsDomain K] [Algebra F E] [Algebra F K] [FiniteDimensional F E] : Fintype (E →ₐ[F] K)
• minpoly.ne_zero_of_finite 📋 Mathlib.FieldTheory.Minpoly.Field
  (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (e : B) [FiniteDimensional A B] : minpoly A e ≠ 0
• minpoly.rootsOfMinPolyPiType 📋 Mathlib.FieldTheory.Minpoly.Field
  (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Ring E] [CommRing K] [IsDomain K] [Algebra F E] [Algebra F K] [FiniteDimensional F E] (φ : E →ₐ[F] K) (x : ↑(Set.range ⇑(Module.finBasis F E))) : { l // l ∈ (minpoly F ↑x).aroots K }
• minpoly.aux_inj_roots_of_min_poly 📋 Mathlib.FieldTheory.Minpoly.Field
  (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Ring E] [CommRing K] [IsDomain K] [Algebra F E] [Algebra F K] [FiniteDimensional F E] : Function.Injective (minpoly.rootsOfMinPolyPiType F E K)
• LinearMap.minpoly_dvd_charpoly 📋 Mathlib.LinearAlgebra.Charpoly.Basic
  {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (f : M →ₗ[K] M) : minpoly K f ∣ f.charpoly
• Module.End.instFintypeEigenvalues 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : Fintype f.Eigenvalues
• Module.End.finite_hasEigenvalue 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : Set.Finite f.HasEigenvalue
• Module.End.finite_spectrum 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : (spectrum K f).Finite
• Module.End.hasEigenvalue_of_isRoot 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} (h : (minpoly K f).IsRoot μ) : f.HasEigenvalue μ
• Module.End.hasEigenvalue_iff_isRoot 📋 Mathlib.LinearAlgebra.Eigenspace.Minpoly
  {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : f.HasEigenvalue μ ↔ (minpoly K f).IsRoot μ
• LinearMap.BilinForm.Nondegenerate.flip 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate) : B.flip.Nondegenerate
• LinearMap.BilinForm.nonDegenerateFlip_iff 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} : B.flip.Nondegenerate ↔ B.Nondegenerate
• LinearMap.BilinForm.symmCompOfNondegenerate 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ B₂ : LinearMap.BilinForm K V) (b₂ : B₂.Nondegenerate) : V →ₗ[K] V
• LinearMap.BilinForm.dualBasis_dualBasis 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (hB' : B.IsSymm) {ι : Type u_10} [Finite ι] [DecidableEq ι] [FiniteDimensional K V] (b : Basis ι K V) : B.dualBasis hB (B.dualBasis hB b) = b
• LinearMap.BilinForm.leftAdjointOfNondegenerate 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) : V →ₗ[K] V
• LinearMap.BilinForm.dualBasis_dualBasis_flip 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) {ι : Type u_10} [Finite ι] [DecidableEq ι] (b : Basis ι K V) : B.dualBasis hB (B.flip.dualBasis ⋯ b) = b
• LinearMap.BilinForm.dualBasis_flip_dualBasis 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) {ι : Type u_10} [Finite ι] [DecidableEq ι] [FiniteDimensional K V] (b : Basis ι K V) : B.flip.dualBasis ⋯ (B.dualBasis hB b) = b
• LinearMap.BilinForm.isAdjointPairLeftAdjointOfNondegenerate 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) : LinearMap.IsAdjointPair B B ⇑(B.leftAdjointOfNondegenerate b φ) ⇑φ
• LinearMap.BilinForm.toDual 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) : V ≃ₗ[K] Module.Dual K V
• LinearMap.BilinForm.isAdjointPair_iff_eq_of_nondegenerate 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (ψ φ : V →ₗ[K] V) : LinearMap.IsAdjointPair B B ⇑ψ ⇑φ ↔ ψ = B.leftAdjointOfNondegenerate b φ
• LinearMap.BilinForm.symmCompOfNondegenerate.eq_1 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ B₂ : LinearMap.BilinForm K V) (b₂ : B₂.Nondegenerate) : B₁.symmCompOfNondegenerate B₂ b₂ = ↑(B₂.toDual b₂).symm ∘ₗ B₁
• LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) {B₂ : LinearMap.BilinForm K V} (b₂ : B₂.Nondegenerate) (v : V) : B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) v) = B₁ v
• LinearMap.BilinForm.symmCompOfNondegenerate_left_apply 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) {B₂ : LinearMap.BilinForm K V} (b₂ : B₂.Nondegenerate) (v w : V) : (B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) w)) v = (B₁ w) v
• LinearMap.BilinForm.toDual_def 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (b : LinearMap.SeparatingLeft B) {m n : V} : ((B.toDual b) m) n = (B m) n
• LinearMap.BilinForm.apply_toDual_symm_apply 📋 Mathlib.LinearAlgebra.BilinearForm.Properties
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {hB : B.Nondegenerate} (f : Module.Dual K V) (v : V) : (B ((B.toDual hB).symm f)) v = f v
• LinearMap.BilinForm.orthogonal_orthogonal 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : Submodule K V) : B.orthogonal (B.orthogonal W) = W
• LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (hB₀ : B.IsRefl) : IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W)
• LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.orthogonal W = ⊥) : W = ⊤
• LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) : IsCompl W (B.orthogonal W)
• LinearMap.BilinForm.orthogonal_eq_top_iff 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) : B.orthogonal W = ⊤ ↔ W = ⊥
• LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) : (B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W)
• LinearMap.BilinForm.orthogonal_eq_bot_iff 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Submodule K V} (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.Nondegenerate) : B.orthogonal W = ⊥ ↔ W = ⊤
• LinearMap.BilinForm.finrank_orthogonal 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : Submodule K V) : Module.finrank K ↥(B.orthogonal W) = Module.finrank K V - Module.finrank K ↥W
• LinearMap.BilinForm.finrank_add_finrank_orthogonal 📋 Mathlib.LinearAlgebra.BilinearForm.Orthogonal
  {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (b₁ : B.IsRefl) (W : Submodule K V) : Module.finrank K ↥W + Module.finrank K ↥(B.orthogonal W) = Module.finrank K V + Module.finrank K ↥(W ⊓ B.orthogonal ⊤)
• IntermediateField.finiteDimensional_right 📋 Mathlib.FieldTheory.IntermediateField.Algebraic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) [FiniteDimensional K L] : FiniteDimensional (↥F) L
• IntermediateField.finiteDimensional_left 📋 Mathlib.FieldTheory.IntermediateField.Algebraic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) [FiniteDimensional K L] : FiniteDimensional K ↥F
• IntermediateField.eq_of_le_of_finrank_eq' 📋 Mathlib.FieldTheory.IntermediateField.Algebraic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [FiniteDimensional (↥F) L] (h_le : F ≤ E) (h_finrank : Module.finrank (↥F) L = Module.finrank (↥E) L) : F = E
• IntermediateField.eq_of_le_of_finrank_le' 📋 Mathlib.FieldTheory.IntermediateField.Algebraic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [FiniteDimensional (↥F) L] (h_le : F ≤ E) (h_finrank : Module.finrank (↥F) L ≤ Module.finrank (↥E) L) : F = E
• im_finiteDimensional 📋 Mathlib.FieldTheory.IntermediateField.Algebraic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (f : L →ₐ[K] L) [FiniteDimensional K ↥E] : FiniteDimensional K ↥(IntermediateField.map f E)
• IntermediateField.finiteDimensional_map 📋 Mathlib.FieldTheory.IntermediateField.Algebraic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (f : L →ₐ[K] L) [FiniteDimensional K ↥E] : FiniteDimensional K ↥(IntermediateField.map f E)
• IntermediateField.eq_of_le_of_finrank_eq 📋 Mathlib.FieldTheory.IntermediateField.Algebraic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [FiniteDimensional K ↥E] (h_le : F ≤ E) (h_finrank : Module.finrank K ↥F = Module.finrank K ↥E) : F = E
• IntermediateField.eq_of_le_of_finrank_le 📋 Mathlib.FieldTheory.IntermediateField.Algebraic
  {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} [hfin : FiniteDimensional K ↥E] (h_le : F ≤ E) (h_finrank : Module.finrank K ↥E ≤ Module.finrank K ↥F) : F = E
• IntermediateField.induction_on_adjoin 📋 Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
  {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (P : IntermediateField F E → Prop) (base : P ⊥) (ih : ∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)) (K : IntermediateField F E) : P K
• IntermediateField.sup_toSubalgebra_of_left 📋 Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
  {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) [FiniteDimensional K ↥E1] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
• IntermediateField.sup_toSubalgebra_of_right 📋 Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
  {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) [FiniteDimensional K ↥E2] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08