Loogle!

Result

Found 2060 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 ↑(Module.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 : Module.Basis ι K V) : Fintype ι
• Module.Basis.finiteDimensional_of_finite 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type w} [Finite ι] (h : Module.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_fact_finrank_eq_two 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [Fact (Module.finrank K V = 2)] : 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.finiteDimensional_pi 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) [DivisionRing K] {ι : Type u_1} [Finite ι] : FiniteDimensional K (ι → K)
• 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 : Module.Basis (↑s) K V) (hs : s.Finite) : FiniteDimensional K V
• 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 : Module.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_singleton 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
  (K : Type u) {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (x : V) : FiniteDimensional K ↥(K ∙ x)
• 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.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.instSubtypeMemSubmoduleMap 📋 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) : Module.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)
• FiniteDimensional.finrank_le_iff_rank_le 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {n : ℕ} : Module.finrank K V ≤ n ↔ Module.rank K V ≤ ↑n
• 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.finrank_lt_iff_rank_lt 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {n : ℕ} : Module.finrank K V < n ↔ Module.rank K V < ↑n
• 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
• AlgHom.bijective 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u_1} {S : Type u_2} [Field K] [Ring S] [IsSimpleRing S] [Algebra K S] [FiniteDimensional K S] (f : S →ₐ[K] S) : Function.Bijective ⇑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 : f.range = ⊤) : FiniteDimensional K V₂
• 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
• 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 ↔ f.ker = ⊥
• 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 ↔ f.range = ⊤
• 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.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} : f.ker = ⊥ ↔ f.range = ⊤
• LinearEquiv.ofInjectiveOfFinrankEq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V' : Type u_1} [AddCommGroup V'] [Module K V'] [FiniteDimensional K V'] (f : V →ₗ[K] V') (hinj : Function.Injective ⇑f) (hrank : Module.finrank K V = Module.finrank K V') : V ≃ₗ[K] V'
• 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.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 ↥f.range
• 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₂)
• 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
• LinearEquiv.coe_ofInjectiveOfFinrankEq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {V' : Type u_1} [AddCommGroup V'] [Module K V'] [FiniteDimensional K V'] (f : V →ₗ[K] V') (hinj : Function.Injective ⇑f) (hrank : Module.finrank K V = Module.finrank K V') : ↑(LinearEquiv.ofInjectiveOfFinrankEq f hinj hrank) = f
• 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
• 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_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)
• 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
• 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.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 f.ker g.ker) : (f ∘ₗ g).ker = f.ker ⊔ g.ker
• 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.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 f.ker) : Submodule.comap f p = p ⊔ f.ker
• 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 => (f i).ker) : (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker
• 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
• Submodule.exists_linearEquiv_restrict_eq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {W W' : Submodule K V} [FiniteDimensional K ↥W] (f : ↥W ≃ₗ[K] ↥W') : ∃ g, ∀ (x : ↥W), ↑(f x) = g ↑x
• CSA.fin_dim 📋 Mathlib.Algebra.BrauerGroup.Defs
  {K : Type u} [Field K] (self : CSA K) : FiniteDimensional K ↑self.toAlgCat
• CSA.mk 📋 Mathlib.Algebra.BrauerGroup.Defs
  {K : Type u} [Field K] (toAlgCat : AlgCat K) [isCentral : Algebra.IsCentral K ↑toAlgCat] [isSimple : IsSimpleRing ↑toAlgCat] [fin_dim : FiniteDimensional K ↑toAlgCat] : CSA K
• basisOfLinearIndependentOfCardEqFinrank' 📋 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) (hb : LinearIndependent K b) (hι : Fintype.card ι = Module.finrank K V) : Module.Basis ι K V
• coe_basisOfLinearIndependentOfCardEqFinrank' 📋 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) (hb : LinearIndependent K b) (hι : Fintype.card ι = Module.finrank K V) : ⇑(basisOfLinearIndependentOfCardEqFinrank' b hb hι) = b
• 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_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
• 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
• 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) : f.ker ≠ ⊥
• 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_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₂} : f.ker = ⊥ ↔ f.range = ⊤
• 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
• 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)
• 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)
• 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
• 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_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
• 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 = ⊤
• 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
• 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
• Submodule.instFiniteDimensionalQuotientMapOfRange 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} {W : Type v'} [DivisionRing K] [AddCommGroup W] [AddCommGroup V] [Module K V] [Module K W] {f : V →ₗ[K] W} (p : Submodule K V) [FiniteDimensional K (V ⧸ p)] [FiniteDimensional K (W ⧸ f.range)] : FiniteDimensional K (W ⧸ Submodule.map f p)
• 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 ↥f.range + Module.finrank K ↥f.ker = Module.finrank K V
• Submodule.instFiniteDimensionalSubtypeMemComapOfKer 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} {W : Type v'} [DivisionRing K] [AddCommGroup W] [AddCommGroup V] [Module K V] [Module K W] {f : V →ₗ[K] W} (p : Submodule K W) [FiniteDimensional K ↥p] [FiniteDimensional K ↥f.ker] : FiniteDimensional K ↥(Submodule.comap f p)
• 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
• basisOfLinearIndependentOfCardEqFinrank'_repr_apply 📋 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) (hb : LinearIndependent K b) (hι : Fintype.card ι = Module.finrank K V) (x : V) : (basisOfLinearIndependentOfCardEqFinrank' b hb hι).repr x = hb.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ⋯) x)
• 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.isCompl_ker_of_disjoint_of_ne_bot 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} [DivisionRing 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} [DivisionRing 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₁
• Module.Dual.eq_of_ker_eq_of_apply_eq 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_1} {V₁ : Type u_2} [DivisionRing 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
• 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))ᵒᵈ
• 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
• 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, (L i).ker ≤ K.ker) : K ∈ Submodule.span 𝕜 (Set.range L)
• 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.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.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.dualCoannihilator_iInf 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_6} (W : ι → Subspace K (Module.Dual K V)) [∀ (i : ι), FiniteDimensional K ↥(W i)] : Submodule.dualCoannihilator (⨅ i, W i) = ⨆ i, Submodule.dualCoannihilator (W i)
• 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.dualCoannihilator_inf 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (W W' : Subspace K (Module.Dual K V)) [FiniteDimensional K ↥W] [FiniteDimensional K ↥W'] : Submodule.dualCoannihilator (W ⊓ W') = Submodule.dualCoannihilator W ⊔ Submodule.dualCoannihilator W'
• 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₁ ⧸ W.dualLift.range
• 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 ⧸ W.dualLift.range) ≃ₗ[K] ↥(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.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)
• 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
• 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 = have bV := Module.Basis.ofVectorSpace K V; ∑ i, bV i ⊗ₜ[K] bV.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))
• instFiniteDimensionalFractionRingOfFinite 📋 Mathlib.RingTheory.Algebraic.Integral
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [Module.IsTorsionFree R S] [Module.Finite R S] : FiniteDimensional (FractionRing R) (FractionRing S)
• algEquivEquivAlgHom 📋 Mathlib.RingTheory.Algebraic.Integral
  (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : Gal(L/K) ≃* (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
• 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)
• 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.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.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.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)
• Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six 📋 Mathlib.Algebra.Exact.Sequence
  {k : Type u_1} [DivisionRing k] {V₀ : Type u₀} [AddCommGroup V₀] [Module k V₀] [FiniteDimensional k V₀] {V₁ : Type u₁} [AddCommGroup V₁] [Module k V₁] [FiniteDimensional k V₁] {V₂ : Type u₂} [AddCommGroup V₂] [Module k V₂] [FiniteDimensional k V₂] {V₃ : Type u₃} [AddCommGroup V₃] [Module k V₃] [FiniteDimensional k V₃] {V₄ : Type u₄} [AddCommGroup V₄] [Module k V₄] [FiniteDimensional k V₄] {V₅ : Type u₅} [AddCommGroup V₅] [Module k V₅] [FiniteDimensional k V₅] (f₀ : V₀ →ₗ[k] V₁) (f₁ : V₁ →ₗ[k] V₂) (f₂ : V₂ →ₗ[k] V₃) (f₃ : V₃ →ₗ[k] V₄) (f₄ : V₄ →ₗ[k] V₅) (inj : Function.Injective ⇑f₀) (exact₁ : Function.Exact ⇑f₀ ⇑f₁) (exact₂ : Function.Exact ⇑f₁ ⇑f₂) (exact₃ : Function.Exact ⇑f₂ ⇑f₃) (exact₄ : Function.Exact ⇑f₃ ⇑f₄) (surj : Function.Surjective ⇑f₄) : ↑(Module.finrank k V₀) - ↑(Module.finrank k V₁) + ↑(Module.finrank k V₂) - ↑(Module.finrank k V₃) + ↑(Module.finrank k V₄) - ↑(Module.finrank k V₅) = 0
• Module.sum_neg_one_pow_finrank_eq_zero_of_exact 📋 Mathlib.Algebra.Exact.Sequence
  {k : Type u_1} [DivisionRing k] {n : ℕ} (V : Fin (n + 2) → Type u_2) [(i : Fin (n + 2)) → AddCommGroup (V i)] [(i : Fin (n + 2)) → Module k (V i)] [∀ (i : Fin (n + 2)), FiniteDimensional k (V i)] (f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ) (inj : Function.Injective ⇑(f 0)) (h_exact : ∀ (i : Fin n), Function.Exact ⇑(f i.castSucc) ⇑(f i.succ)) (surj : Function.Surjective ⇑(f (Fin.last n))) : ∑ i, (-1) ^ ↑i * ↑(Module.finrank k (V i)) = 0
• 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)
• 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.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
• Module.End.IsSemisimple.pow 📋 Mathlib.LinearAlgebra.Semisimple
  {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] (hf : f.IsSemisimple) (n : ℕ) : (f ^ n).IsSemisimple
• Module.End.IsSemisimple.mul_of_commute 📋 Mathlib.LinearAlgebra.Semisimple
  {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f g : Module.End K M} [FiniteDimensional K M] [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple) : (f * g).IsSemisimple
• Module.End.IsSemisimple.sub_of_commute 📋 Mathlib.LinearAlgebra.Semisimple
  {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f g : Module.End K M} [FiniteDimensional K M] [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple) : (f - g).IsSemisimple
• Module.End.IsSemisimple.add_of_commute 📋 Mathlib.LinearAlgebra.Semisimple
  {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f g : Module.End K M} [FiniteDimensional K M] [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple) : (f + g).IsSemisimple
• Module.End.IsSemisimple.minpoly_squarefree 📋 Mathlib.LinearAlgebra.Semisimple
  {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] (hf : f.IsSemisimple) : Squarefree (minpoly K f)
• Module.End.IsSemisimple.aeval 📋 Mathlib.LinearAlgebra.Semisimple
  {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] (hf : f.IsSemisimple) (p : Polynomial K) : ((Polynomial.aeval f) p).IsSemisimple
• Module.End.IsSemisimple.of_mem_adjoin_singleton 📋 Mathlib.LinearAlgebra.Semisimple
  {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] (hf : f.IsSemisimple) {a : Module.End K M} (ha : a ∈ K[f]) : a.IsSemisimple
• Module.End.IsSemisimple.of_mem_adjoin_pair 📋 Mathlib.LinearAlgebra.Semisimple
  {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f g : Module.End K M} [FiniteDimensional K M] [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple) {a : Module.End K M} (ha : a ∈ K[f, g]) : a.IsSemisimple
• LieAlgebra.ad_isSemisimple_of_isSemisimple 📋 Mathlib.Algebra.Lie.AdjointAction.Basic
  {K : Type u_1} {V : Type u_2} [Field K] [PerfectField K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {a : Module.End K V} (ha : a.IsSemisimple) : ((LieAlgebra.ad K (Module.End K V)) a).IsSemisimple
• Module.End.isNilpotent_isSemisimple_unique 📋 Mathlib.LinearAlgebra.JordanChevalley
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [PerfectField K] {n₁ s₁ n₂ s₂ : Module.End K V} (hn₁ : IsNilpotent n₁) (hs₁ : s₁.IsSemisimple) (hn₂ : IsNilpotent n₂) (hs₂ : s₂.IsSemisimple) (hc₁ : Commute n₁ s₁) (hc₂ : Commute n₂ s₂) (h : n₁ + s₁ = n₂ + s₂) : n₁ = n₂ ∧ s₁ = s₂
• Module.End.exists_isNilpotent_isSemisimple 📋 Mathlib.LinearAlgebra.JordanChevalley
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} [FiniteDimensional K V] [PerfectField K] : ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
• LieAlgebra.ad_mem_adjoin_of_isNilpotent 📋 Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
  {K : Type u_1} {V : Type u_2} [Field K] [PerfectField K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {n s : Module.End K V} (hc : Commute n s) (hn : IsNilpotent n) (hs : s.IsSemisimple) : (LieAlgebra.ad K (Module.End K V)) n ∈ K[(LieAlgebra.ad K (Module.End K V)) (n + s)]
• LieAlgebra.ad_mem_adjoin_of_isSemisimple 📋 Mathlib.Algebra.Lie.AdjointAction.JordanChevalley
  {K : Type u_1} {V : Type u_2} [Field K] [PerfectField K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {n s : Module.End K V} (hc : Commute n s) (hn : IsNilpotent n) (hs : s.IsSemisimple) : (LieAlgebra.ad K (Module.End K V)) s ∈ K[(LieAlgebra.ad K (Module.End K V)) (n + s)]
• AlgEquiv.fintype 📋 Mathlib.FieldTheory.Fixed
  (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V] [FiniteDimensional K V] : Fintype Gal(V/K)
• FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield 📋 Mathlib.FieldTheory.Fixed
  (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Finite G] : FiniteDimensional (↥(FixedPoints.subfield G F)) F
• AlgEquiv.card_le 📋 Mathlib.FieldTheory.Fixed
  {F : Type u_2} {K : Type u_3} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] : Fintype.card Gal(K/F) ≤ Module.finrank F K
• AlgHom.card_le 📋 Mathlib.FieldTheory.Fixed
  {F : Type u_2} {K : Type u_3} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] : Fintype.card (K →ₐ[F] K) ≤ Module.finrank F K
• cardinalMk_algHom 📋 Mathlib.FieldTheory.Fixed
  (K : Type u) (V : Type v) (W : Type w) [Field K] [Ring V] [Algebra K V] [FiniteDimensional K V] [Field W] [Algebra K W] : Cardinal.mk (V →ₐ[K] W) ≤ ↑(Module.finrank W (V →ₗ[K] W))
• finrank_algHom 📋 Mathlib.FieldTheory.Fixed
  (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V] [FiniteDimensional K V] : Fintype.card (V →ₐ[K] V) ≤ Module.finrank V (V →ₗ[K] V)
• 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.finrank_le_of_le_left 📋 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 : F ≤ E) : Module.finrank (↥E) L ≤ Module.finrank (↥F) L
• IntermediateField.finrank_lt_of_gt 📋 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 : F < E) : Module.finrank (↥E) L < Module.finrank (↥F) L
• 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_iff_finrank_eq_of_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) : F = E ↔ Module.finrank (↥F) L = Module.finrank (↥E) L
• 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
• 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.finrank_le_of_le_right 📋 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 : F ≤ E) : Module.finrank K ↥F ≤ Module.finrank K ↥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_iff_finrank_eq_of_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 K ↥E] (h_le : F ≤ E) : F = E ↔ Module.finrank K ↥F = Module.finrank K ↥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
• Polynomial.IsSplittingField.finiteDimensional 📋 Mathlib.FieldTheory.SplittingField.IsSplittingField
  {K : Type v} (L : Type w) [Field K] [Field L] [Algebra K L] (f : Polynomial K) [Polynomial.IsSplittingField K L f] : FiniteDimensional K L

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision cecebc3