Loogle!
Result
Found 44 definitions mentioning Top.top and Module.finrank.
- finrank_top 📋 Mathlib.LinearAlgebra.Dimension.Finrank
(R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] : Module.finrank R ↥⊤ = Module.finrank R M - finrank_le_of_span_eq_top 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {ι : Type u_2} [Fintype ι] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) : Module.finrank R M ≤ Fintype.card ι - span_lt_top_of_card_lt_finrank 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] {s : Set M} [Fintype ↑s] (card_lt : s.toFinset.card < Module.finrank R M) : Submodule.span R s < ⊤ - Submodule.lt_top_of_finrank_lt_finrank 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} (lt : Module.finrank R ↥s < Module.finrank R M) : s < ⊤ - subalgebra_top_finrank_eq_submodule_top_finrank 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{F : Type u_2} {E : Type u_3} [CommRing F] [Ring E] [Algebra F E] : Module.finrank F ↥⊤ = Module.finrank F ↥⊤ - finrank_eq_one_iff_of_nonzero 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (nz : v ≠ 0) : Module.finrank K V = 1 ↔ Submodule.span K {v} = ⊤ - Submodule.eq_top_of_finrank_eq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Defs
{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 = ⊤ - Module.finrank_le_one_iff_top_isPrincipal 📋 Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
{K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] : Module.finrank K V ≤ 1 ↔ ⊤.IsPrincipal - Subalgebra.bot_eq_top_of_finrank_eq_one 📋 Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
{F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] [Nontrivial E] [Module.Free F E] : Module.finrank F E = 1 → ⊥ = ⊤ - Subalgebra.bot_eq_top_iff_finrank_eq_one 📋 Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
{F : Type u_1} {E : Type u_2} [CommRing F] [StrongRankCondition F] [Ring E] [Algebra F E] [Nontrivial E] [Module.Free F E] : ⊥ = ⊤ ↔ Module.finrank F E = 1 - basisOfTopLeSpanOfCardEqFinrank 📋 Mathlib.LinearAlgebra.Dimension.DivisionRing
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [Fintype ι] (b : ι → V) (le_span : ⊤ ≤ Submodule.span K (Set.range b)) (card_eq : Fintype.card ι = Module.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} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [Fintype ι] {b : ι → V} (spans : ⊤ ≤ Submodule.span K (Set.range b)) (card_eq : Fintype.card ι = Module.finrank K V) : LinearIndependent K b - setBasisOfTopLeSpanOfCardEqFinrank 📋 Mathlib.LinearAlgebra.Dimension.DivisionRing
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Fintype ↑s] (le_span : ⊤ ≤ Submodule.span K s) (card_eq : s.toFinset.card = Module.finrank K V) : Basis (↑s) K V - finsetBasisOfTopLeSpanOfCardEqFinrank 📋 Mathlib.LinearAlgebra.Dimension.DivisionRing
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (le_span : ⊤ ≤ Submodule.span K ↑s) (card_eq : s.card = Module.finrank K V) : Basis { x // x ∈ s } K V - coe_basisOfTopLeSpanOfCardEqFinrank 📋 Mathlib.LinearAlgebra.Dimension.DivisionRing
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [Fintype ι] (b : ι → V) (le_span : ⊤ ≤ Submodule.span K (Set.range b)) (card_eq : Fintype.card ι = Module.finrank K V) : ⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b - setBasisOfTopLeSpanOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.Dimension.DivisionRing
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Fintype ↑s] (le_span : ⊤ ≤ Submodule.span K s) (card_eq : s.toFinset.card = Module.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} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (le_span : ⊤ ≤ Submodule.span K ↑s) (card_eq : s.card = Module.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✝) - span_eq_top_of_linearIndependent_of_card_eq_finrank 📋 Mathlib.LinearAlgebra.FiniteDimensional
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.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} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.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} [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
{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.eq_top_of_disjoint 📋 Mathlib.LinearAlgebra.FiniteDimensional
{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 ↥s + Module.finrank K ↥t = Module.finrank K V) (hdisjoint : 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} [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 = ⊤ - 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.finrank_top 📋 Mathlib.FieldTheory.Adjoin
{F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.finrank (↥⊤) E = 1 - IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one 📋 Mathlib.FieldTheory.Adjoin
{F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (h : ∀ (x : E), Module.finrank F ↥F⟮x⟯ = 1) : ⊥ = ⊤ - IntermediateField.finrank_top' 📋 Mathlib.FieldTheory.Adjoin
{F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.finrank F ↥⊤ = Module.finrank F E - IntermediateField.bot_eq_top_of_finrank_adjoin_le_one 📋 Mathlib.FieldTheory.Adjoin
{F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (h : ∀ (x : E), Module.finrank F ↥F⟮x⟯ ≤ 1) : ⊥ = ⊤ - 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} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [FiniteDimensional k V] [Fintype ι] {p : ι → P} (hi : AffineIndependent k p) (hc : Fintype.card ι = Module.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} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] [FiniteDimensional k V] [Fintype ι] {p : ι → P} (hi : AffineIndependent k p) : affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = Module.finrank k V + 1 - Affine.Simplex.span_eq_top 📋 Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
{k : Type u_1} {V : Type u_2} [DivisionRing k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {n : ℕ} (T : Affine.Simplex k V n) (hrank : Module.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} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] (α : E) : F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = Module.finrank F E - Field.primitive_element_iff_minpoly_degree_eq 📋 Mathlib.FieldTheory.PrimitiveElement
(F : Type u_3) {E : Type u_4} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] (α : E) : F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = ↑(Module.finrank F E) - IsGalois.tfae 📋 Mathlib.FieldTheory.Galois.Basic
{F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] : [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = Module.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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {r : ℝ} (hnr : ↑(Module.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} [Field K] [Field L] [Algebra K L] (E : Type u_1) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K L] [Algebra.IsSeparable K L] {x : L} (hxL : Algebra.adjoin K {x} = ⊤) {r : ℕ} (hr : r < Module.finrank K L) : ∑ σ : L →ₐ[K] E, 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) [Field K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) [IsGalois K L] [IsCyclic (L ≃ₐ[K] L)] : ∃ α, α ^ Module.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} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] {a : K} {α : L} (ha : α ^ Module.finrank K L = (algebraMap K L) a) (hα : K⟮α⟯ = ⊤) : Irreducible (Polynomial.X ^ Module.finrank K L - Polynomial.C a) - isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top 📋 Mathlib.FieldTheory.KummerExtension
{K : Type u} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) {a : K} {α : L} (ha : α ^ Module.finrank K L = (algebraMap K L) a) (hα : K⟮α⟯ = ⊤) : Polynomial.IsSplittingField K L (Polynomial.X ^ Module.finrank K L - Polynomial.C a) - isCyclic_tfae 📋 Mathlib.FieldTheory.KummerExtension
(K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) : [IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L), ∃ a, Irreducible (Polynomial.X ^ Module.finrank K L - Polynomial.C a) ∧ Polynomial.IsSplittingField K L (Polynomial.X ^ Module.finrank K L - Polynomial.C a), ∃ α, α ^ Module.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE - Subfield.relfinrank_top_right 📋 Mathlib.FieldTheory.Relrank
{E : Type v} [Field E] (A : Subfield E) : A.relfinrank ⊤ = Module.finrank (↥A) E - IntermediateField.relfinrank_top_right 📋 Mathlib.FieldTheory.Relrank
{F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A : IntermediateField F E) : A.relfinrank ⊤ = Module.finrank (↥A) E - contMDiff_coe_sphere 📋 Mathlib.Geometry.Manifold.Instances.Sphere
{E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.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} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ fun x => -x
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:
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 ?aIf 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 ?bBy 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_tsumeven though the hypothesisf i < g iis 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 provided by the Lean FRO.
This is Loogle revision 026c9d9 serving mathlib revision 3961c23