Loogle!
Result
Found 41 definitions mentioning FiniteDimensional.finrank and Top.top.
- finrank_top Mathlib.LinearAlgebra.Dimension.Finrank
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], FiniteDimensional.finrank R ↥⊤ = FiniteDimensional.finrank R M - span_lt_top_of_card_lt_finrank Mathlib.LinearAlgebra.Dimension.Constructions
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : StrongRankCondition R] {s : Set M} [inst_4 : Fintype ↑s], s.toFinset.card < FiniteDimensional.finrank R M → Submodule.span R s < ⊤ - Submodule.lt_top_of_finrank_lt_finrank Mathlib.LinearAlgebra.Dimension.Constructions
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Submodule R M}, FiniteDimensional.finrank R ↥s < FiniteDimensional.finrank R M → s < ⊤ - subalgebra_top_finrank_eq_submodule_top_finrank Mathlib.LinearAlgebra.Dimension.Constructions
∀ {F : Type u_2} {E : Type u_3} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E], FiniteDimensional.finrank F ↥⊤ = FiniteDimensional.finrank F ↥⊤ - basisOfTopLeSpanOfCardEqFinrank Mathlib.LinearAlgebra.Dimension.DivisionRing
{K : Type u} → {V : Type v} → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → {ι : Type u_2} → [inst_3 : Fintype ι] → (b : ι → V) → ⊤ ≤ Submodule.span K (Set.range b) → Fintype.card ι = FiniteDimensional.finrank K V → Basis ι K V - linearIndependent_of_top_le_span_of_card_eq_finrank Mathlib.LinearAlgebra.Dimension.DivisionRing
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_2} [inst_3 : Fintype ι] {b : ι → V}, ⊤ ≤ Submodule.span K (Set.range b) → Fintype.card ι = FiniteDimensional.finrank K V → LinearIndependent K b - setBasisOfTopLeSpanOfCardEqFinrank Mathlib.LinearAlgebra.Dimension.DivisionRing
{K : Type u} → {V : Type v} → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → {s : Set V} → [inst_3 : Fintype ↑s] → ⊤ ≤ Submodule.span K s → s.toFinset.card = FiniteDimensional.finrank K V → Basis (↑s) K V - finsetBasisOfTopLeSpanOfCardEqFinrank Mathlib.LinearAlgebra.Dimension.DivisionRing
{K : Type u} → {V : Type v} → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → {s : Finset V} → ⊤ ≤ Submodule.span K ↑s → s.card = FiniteDimensional.finrank K V → Basis { x // x ∈ s } K V - coe_basisOfTopLeSpanOfCardEqFinrank Mathlib.LinearAlgebra.Dimension.DivisionRing
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_2} [inst_3 : Fintype ι] (b : ι → V) (le_span : ⊤ ≤ Submodule.span K (Set.range b)) (card_eq : Fintype.card ι = FiniteDimensional.finrank K V), ⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b - setBasisOfTopLeSpanOfCardEqFinrank_repr_apply Mathlib.LinearAlgebra.Dimension.DivisionRing
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V} [inst_3 : Fintype ↑s] (le_span : ⊤ ≤ Submodule.span K s) (card_eq : s.toFinset.card = FiniteDimensional.finrank K V) (a : V), (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = ⋯.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a) - finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply Mathlib.LinearAlgebra.Dimension.DivisionRing
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Finset V} (le_span : ⊤ ≤ Submodule.span K ↑s) (card_eq : s.card = FiniteDimensional.finrank K V) (a : V), (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = ⋯.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a) - Module.finrank_le_one_iff_top_isPrincipal Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : FiniteDimensional K V], FiniteDimensional.finrank K V ≤ 1 ↔ ⊤.IsPrincipal - span_eq_top_of_linearIndependent_of_card_eq_finrank Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1} [inst_3 : Nonempty ι] [inst_4 : Fintype ι] {b : ι → V}, LinearIndependent K b → Fintype.card ι = FiniteDimensional.finrank K V → Submodule.span K (Set.range b) = ⊤ - LinearIndependent.span_eq_top_of_card_eq_finrank Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1} [inst_3 : Nonempty ι] [inst_4 : Fintype ι] {b : ι → V}, LinearIndependent K b → Fintype.card ι = FiniteDimensional.finrank K V → Submodule.span K (Set.range b) = ⊤ - LinearIndependent.span_eq_top_of_card_eq_finrank' Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1} [inst_3 : Fintype ι] [inst_4 : FiniteDimensional K V] {b : ι → V}, LinearIndependent K b → Fintype.card ι = FiniteDimensional.finrank K V → Submodule.span K (Set.range b) = ⊤ - finrank_eq_one_iff_of_nonzero Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V), v ≠ 0 → (FiniteDimensional.finrank K V = 1 ↔ Submodule.span K {v} = ⊤) - Subalgebra.bot_eq_top_of_finrank_eq_one Mathlib.LinearAlgebra.FiniteDimensional
∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] [inst_3 : Nontrivial E], FiniteDimensional.finrank F E = 1 → ⊥ = ⊤ - Subalgebra.bot_eq_top_iff_finrank_eq_one Mathlib.LinearAlgebra.FiniteDimensional
∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] [inst_3 : Nontrivial E], ⊥ = ⊤ ↔ FiniteDimensional.finrank F E = 1 - Submodule.eq_top_of_finrank_eq Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : FiniteDimensional K V] {S : Submodule K V}, FiniteDimensional.finrank K ↥S = FiniteDimensional.finrank K V → S = ⊤ - Submodule.finrank_lt Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : FiniteDimensional K V] {s : Submodule K V}, s < ⊤ → FiniteDimensional.finrank K ↥s < FiniteDimensional.finrank K V - Submodule.eq_top_of_disjoint Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : FiniteDimensional K V] (s t : Submodule K V), FiniteDimensional.finrank K ↥s + FiniteDimensional.finrank K ↥t = FiniteDimensional.finrank K V → Disjoint s t → s ⊔ t = ⊤ - LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank Mathlib.LinearAlgebra.FiniteDimensional
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'} [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : FiniteDimensional K V] [inst_6 : FiniteDimensional K V₂], FiniteDimensional.finrank K V = FiniteDimensional.finrank K V₂ → ∀ {f : V →ₗ[K] V₂}, LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤ - IntermediateField.finrank_top Mathlib.FieldTheory.Adjoin
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], FiniteDimensional.finrank (↥⊤) E = 1 - IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one Mathlib.FieldTheory.Adjoin
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], (∀ (x : E), FiniteDimensional.finrank F ↥F⟮x⟯ = 1) → ⊥ = ⊤ - IntermediateField.finrank_top' Mathlib.FieldTheory.Adjoin
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], FiniteDimensional.finrank F ↥⊤ = FiniteDimensional.finrank F E - IntermediateField.bot_eq_top_of_finrank_adjoin_le_one Mathlib.FieldTheory.Adjoin
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [inst_3 : FiniteDimensional F E], (∀ (x : E), FiniteDimensional.finrank F ↥F⟮x⟯ ≤ 1) → ⊥ = ⊤ - LinearMap.BilinForm.finrank_add_finrank_orthogonal Mathlib.LinearAlgebra.BilinearForm.Orthogonal
∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [inst_3 : FiniteDimensional K V] {B : LinearMap.BilinForm K V} {W : Subspace K V}, B.IsRefl → FiniteDimensional.finrank K ↥W + FiniteDimensional.finrank K ↥(B.orthogonal W) = FiniteDimensional.finrank K V + FiniteDimensional.finrank K ↥(W ⊓ B.orthogonal ⊤) - AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : FiniteDimensional k V] [inst_5 : Fintype ι] {p : ι → P}, AffineIndependent k p → Fintype.card ι = FiniteDimensional.finrank k V + 1 → vectorSpan k (Set.range p) = ⊤ - AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : FiniteDimensional k V] [inst_5 : Fintype ι] {p : ι → P}, AffineIndependent k p → (affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = FiniteDimensional.finrank k V + 1) - Affine.Simplex.span_eq_top Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
∀ {k : Type u_1} {V : Type u_2} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [inst_3 : FiniteDimensional k V] {n : ℕ} (T : Affine.Simplex k V n), FiniteDimensional.finrank k V = n → affineSpan k (Set.range T.points) = ⊤ - Field.primitive_element_iff_minpoly_natDegree_eq Mathlib.FieldTheory.PrimitiveElement
∀ (F : Type u_3) {E : Type u_4} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [inst_3 : FiniteDimensional F E] (α : E), F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = FiniteDimensional.finrank F E - Field.primitive_element_iff_minpoly_degree_eq Mathlib.FieldTheory.PrimitiveElement
∀ (F : Type u_3) {E : Type u_4} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [inst_3 : FiniteDimensional F E] (α : E), F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = ↑(FiniteDimensional.finrank F E) - IsGalois.tfae Mathlib.FieldTheory.Galois
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [inst_3 : FiniteDimensional F E], [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E, ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE - finite_integral_one_add_norm Mathlib.Analysis.SpecialFunctions.JapaneseBracket
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : μ.IsAddHaarMeasure] {r : ℝ}, ↑(FiniteDimensional.finrank ℝ E) < r → ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ⊤ - sum_smul_minpolyDiv_eq_X_pow Mathlib.FieldTheory.Minpoly.MinpolyDiv
∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : Type u_1) [inst_3 : Field E] [inst_4 : Algebra K E] [inst_5 : IsAlgClosed E] [inst_6 : FiniteDimensional K L] [inst_7 : IsSeparable K L] {x : L}, Algebra.adjoin K {x} = ⊤ → ∀ {r : ℕ}, r < FiniteDimensional.finrank K L → (Finset.univ.sum fun σ => Polynomial.map (↑σ) ((x ^ r / (Polynomial.aeval x) (Polynomial.derivative (minpoly K x))) • minpolyDiv K x)) = Polynomial.X ^ r - exists_root_adjoin_eq_top_of_isCyclic Mathlib.FieldTheory.KummerExtension
∀ (K : Type u) [inst : Field K] (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : IsGalois K L] [inst_4 : FiniteDimensional K L] [inst_5 : IsCyclic (L ≃ₐ[K] L)], (primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty → ∃ α, α ^ FiniteDimensional.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤ - irreducible_X_pow_sub_C_of_root_adjoin_eq_top Mathlib.FieldTheory.KummerExtension
∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : FiniteDimensional K L] {a : K} {α : L}, α ^ FiniteDimensional.finrank K L = (algebraMap K L) a → K⟮α⟯ = ⊤ → Irreducible (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a) - isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top Mathlib.FieldTheory.KummerExtension
∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : FiniteDimensional K L], (primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty → ∀ {a : K} {α : L}, α ^ FiniteDimensional.finrank K L = (algebraMap K L) a → K⟮α⟯ = ⊤ → Polynomial.IsSplittingField K L (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a) - isCyclic_tfae Mathlib.FieldTheory.KummerExtension
∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : FiniteDimensional K L], (primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty → [IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L), ∃ a, Irreducible (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a) ∧ Polynomial.IsSplittingField K L (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a), ∃ α, α ^ FiniteDimensional.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE - contMDiff_coe_sphere Mathlib.Geometry.Manifold.Instances.Sphere
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ} [inst_2 : Fact (FiniteDimensional.finrank ℝ E = n + 1)], ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) ⊤ Subtype.val - contMDiff_neg_sphere Mathlib.Geometry.Manifold.Instances.Sphere
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ} [inst_2 : Fact (FiniteDimensional.finrank ℝ E = n + 1)], ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ fun x => -x
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the VS
Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.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
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 findtsum_lt_tsum
even though the hypothesisf 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, _ * _, _ ^ _, |- _ < _ → _
woould 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 currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision fa2ddf5
serving mathlib revision 7bda946