Loogle!

Result

Found 1071 declarations mentioning Module.Finite. Of these, only the first 200 are shown.

Module.Finite 📋 Mathlib.RingTheory.Finiteness.Defs
(R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
AddMonoid.FG.to_moduleFinite_nat 📋 Mathlib.RingTheory.Finiteness.Defs
{M : Type u_4} [AddCommMonoid M] [AddMonoid.FG M] : Module.Finite ℕ M
Module.Finite.iff_addMonoid_fg 📋 Mathlib.RingTheory.Finiteness.Defs
{M : Type u_4} [AddCommMonoid M] : Module.Finite ℕ M ↔ AddMonoid.FG M
Module.Finite.iff_addGroup_fg 📋 Mathlib.RingTheory.Finiteness.Defs
{G : Type u_4} [AddCommGroup G] : Module.Finite ℤ G ↔ AddGroup.FG G
AddMonoid.FG.to_moduleFinite_int 📋 Mathlib.RingTheory.Finiteness.Defs
{G : Type u_4} [AddCommGroup G] [AddMonoid.FG G] : Module.Finite ℤ G
Module.Finite.fg_top 📋 Mathlib.RingTheory.Finiteness.Defs
{R : Type u_1} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : Module R M} [self : Module.Finite R M] : ⊤.FG
Module.Finite.of_fg_top 📋 Mathlib.RingTheory.Finiteness.Defs
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (fg_top : ⊤.FG) : Module.Finite R M
Module.finite_def 📋 Mathlib.RingTheory.Finiteness.Defs
{R : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Module.Finite R M ↔ ⊤.FG
Module.Finite.exists_fin 📋 Mathlib.RingTheory.Finiteness.Defs
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ∃ n s, Submodule.span R (Set.range s) = ⊤
RingHom.finite_algebraMap 📋 Mathlib.RingTheory.Finiteness.Defs
{A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] : (algebraMap A B).Finite ↔ Module.Finite A B
Module.Finite.self 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_1) [Semiring R] : Module.Finite R R
Module.Finite.of_finite 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Finite M] : Module.Finite R M
Module.Finite.instMulOpposite 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Module.Finite R Mᵐᵒᵖ
Module.Finite.ulift 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Module.Finite R (ULift.{u_5, u_3} M)
Module.Finite.instIsCoatomicSubmodule 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : IsCoatomic (Submodule R M)
Module.Finite.shrink 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Small.{u, u_3} M] : Module.Finite R (Shrink.{u, u_3} M)
Module.Finite.Module.finite_shrink 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Small.{u, u_3} M] : Module.Finite R (Shrink.{u, u_3} M)
Module.Finite.of_pi 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} [Semiring R] {ι : Type u_5} (M : ι → Type u_6) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Module.Finite R ((i : ι) → M i)] (i : ι) : Module.Finite R (M i)
Module.Finite.pi 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} [Semiring R] {ι : Type u_5} {M : ι → Type u_6} [Finite ι] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [h : ∀ (i : ι), Module.Finite R (M i)] : Module.Finite R ((i : ι) → M i)
Module.Finite.pi_iff 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} [Semiring R] {ι : Type u_5} {M : ι → Type u_6} [Finite ι] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : Module.Finite R ((i : ι) → M i) ↔ ∀ (i : ι), Module.Finite R (M i)
Module.Finite.equiv 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] (e : M ≃ₗ[R] N) : Module.Finite R N
Module.Finite.equiv_iff 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : Module.Finite R M ↔ Module.Finite R N
Module.Finite.of_fg 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : N.FG → Module.Finite R ↥N
Submodule.FG.of_finite 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} [Module.Finite R ↥N] : N.FG
Module.Finite.iff_fg 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : Module.Finite R ↥N ↔ N.FG
Submodule.fg_range 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} {P : Type u_4} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} [RingHomSurjective σ] [Module.Finite R M] (f : M →ₛₗ[σ] P) : f.range.FG
Module.Finite.span_of_finite 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {A : Set M} (hA : A.Finite) : Module.Finite R ↥(Submodule.span R A)
Module.Finite.top_left 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Module.Finite (↥⊤) M
Module.Finite.of_surjective 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_6} {P : Type u_5} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} [hM : Module.Finite R M] (f : M →ₛₗ[σ] P) (hf : Function.Surjective ⇑f) : Module.Finite S P
Module.Finite.bot 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] : Module.Finite R ↥⊥
Module.Finite.span_singleton 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : Module.Finite R ↥(R ∙ x)
Module.Finite.span_finset 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Finset M) : Module.Finite R ↥(Submodule.span R ↑s)
LinearMap.finite_iff_of_bijective 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_6} {P : Type u_5} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} [RingHomSurjective σ] (f : M →ₛₗ[σ] P) (hf : Function.Bijective ⇑f) : Module.Finite R M ↔ Module.Finite S P
Module.Finite.top 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Module.Finite R ↥⊤
RingHom.Finite.instFinite 📋 Mathlib.RingTheory.Finiteness.Basic
{A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (h : A ≃+* B) : Module.Finite A B
Module.Finite.of_restrictScalars_finite 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_5) (A : Type u_6) (M : Type u_7) [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMul R A] [IsScalarTower R A M] [hM : Module.Finite R M] : Module.Finite A M
Module.Finite.range 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] (f : M →ₗ[R] N) : Module.Finite R ↥f.range
instModuleFinite 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {E : Type u_2} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [Module.Finite R E] : Module.Finite (Nonneg R) E
Module.Finite.trans 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_5} (A : Type u_6) (M : Type u_7) [Semiring R] [Semiring A] [Module R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [Module.Finite R A] [Module.Finite A M] : Module.Finite R M
Module.Finite.map 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (p : Submodule R M) [Module.Finite R ↥p] (f : M →ₗ[R] N) : Module.Finite R ↥(Submodule.map f p)
Module.Finite.quotient 📋 Mathlib.RingTheory.Finiteness.Basic
(R : Type u_5) {A : Type u_6} {M : Type u_7} [Semiring R] [AddCommGroup M] [Ring A] [Module A M] [Module R M] [SMul R A] [IsScalarTower R A M] [Module.Finite R M] (N : Submodule A M) : Module.Finite R (M ⧸ N)
Submodule.FG.restrictScalars 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Module R A] [Module A M] [IsScalarTower R A M] {S : Submodule A M} [Module.Finite R A] (hS : S.FG) : (Submodule.restrictScalars R S).FG
Submodule.FG.restrictScalars_iff 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {A : Type u_3} [Semiring A] [Module R A] [Module A M] [IsScalarTower R A M] {S : Submodule A M} [Module.Finite R A] : (Submodule.restrictScalars R S).FG ↔ S.FG
Submodule.finite_finset_sup 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_2} {V : Type u_3} [Ring R] [AddCommGroup V] [Module R V] {ι : Type u_1} (s : Finset ι) (S : ι → Submodule R V) [∀ (i : ι), Module.Finite R ↥(S i)] : Module.Finite R ↥(s.sup S)
Submodule.finite_sup 📋 Mathlib.RingTheory.Finiteness.Basic
{R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] (S₁ S₂ : Submodule R V) [h₁ : Module.Finite R ↥S₁] [h₂ : Module.Finite R ↥S₂] : Module.Finite R ↥(S₁ ⊔ S₂)
Module.Finite.of_equiv_equiv 📋 Mathlib.RingTheory.Finiteness.Basic
{A₁ : Type u_5} {B₁ : Type u_6} {A₂ : Type u_7} {B₂ : Type u_8} [CommSemiring A₁] [CommSemiring B₁] [CommSemiring A₂] [Semiring B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂) (he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)) [Module.Finite A₁ B₁] : Module.Finite A₂ B₂
Module.Finite.reprₛ 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u) (M : Type u_1) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Type u
Module.finite_of_finite 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] [Module.Finite R M] : Finite M
Module.finite_iff_finite 📋 Mathlib.RingTheory.Finiteness.Cardinality
{R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] : Module.Finite R M ↔ Finite M
Module.Finite.repr 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u) (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Type u
Module.Finite.finite_basis 📋 Mathlib.RingTheory.Finiteness.Cardinality
{R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {ι : Type u_3} [Module.Finite R M] (b : Module.Basis ι R M) : Finite ι
Module.not_finite_of_infinite_basis 📋 Mathlib.RingTheory.Finiteness.Cardinality
{R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {ι : Type u_3} [Infinite ι] (b : Module.Basis ι R M) : ¬Module.Finite R M
Module.Finite.exists_fin' 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ∃ n f, Function.Surjective ⇑f
Module.Finite.exists_fin_quot_equiv 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u_3) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ n S, Nonempty (((Fin n → R) ⧸ S) ≃ₗ[R] M)
Module.Finite.kerRepr 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u) (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Submodule R (Fin ⋯.choose → R)
Module.Finite.reprEquiv 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u) (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.Finite.repr R M ≃ₗ[R] M
Module.Finite.kerReprₛ 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u) (M : Type u_1) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ModuleCon R (Fin ⋯.choose → R)
Module.Finite.reprEquivₛ 📋 Mathlib.RingTheory.Finiteness.Cardinality
(R : Type u) (M : Type u_1) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Module.Finite.reprₛ R M ≃ₗ[R] M
FreeAbelianGroup.instFiniteInt 📋 Mathlib.RingTheory.Finiteness.Finsupp
{σ : Type u_1} [Finite σ] : Module.Finite ℤ (FreeAbelianGroup σ)
AddMonoidAlgebra.moduleFinite 📋 Mathlib.RingTheory.Finiteness.Finsupp
{M : Type u_1} {R : Type u_2} {S : Type u_3} [Finite M] [Semiring R] [Semiring S] [Module R S] [Module.Finite R S] : Module.Finite R (AddMonoidAlgebra S M)
MonoidAlgebra.moduleFinite 📋 Mathlib.RingTheory.Finiteness.Finsupp
{M : Type u_1} {R : Type u_2} {S : Type u_3} [Finite M] [Semiring R] [Semiring S] [Module R S] [Module.Finite R S] : Module.Finite R (MonoidAlgebra S M)
Module.Finite.finsupp 📋 Mathlib.RingTheory.Finiteness.Finsupp
{R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] {ι : Type u_1} [Finite ι] [Module.Finite R V] : Module.Finite R (ι →₀ V)
Module.Finite.of_submodule_quotient 📋 Mathlib.RingTheory.Finiteness.Finsupp
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [Module.Finite R ↥N] [Module.Finite R (M ⧸ N)] : Module.Finite R M
Module.Finite.of_exact 📋 Mathlib.RingTheory.Finiteness.Finsupp
{R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h_exact : Function.Exact ⇑f ⇑g) (h_surj : Function.Surjective ⇑g) [Module.Finite R M] [Module.Finite R P] : Module.Finite R N
LinearMap.finsuppLinearMap_bijective_of_moduleFinite 📋 Mathlib.RingTheory.Finiteness.Finsupp
(R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (S : Type u_5) [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] [Module.Finite R M] : Function.Bijective ⇑(LinearMap.finsuppLinearMap S)
Module.IsNoetherian.finite 📋 Mathlib.RingTheory.Noetherian.Basic
(R : Type u_1) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] : Module.Finite R M
isNoetherian_of_isNoetherianRing_of_finite 📋 Mathlib.RingTheory.Noetherian.Basic
(R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : IsNoetherian R M
Module.instFiniteSubtypeMemIdealOfIsNoetherian 📋 Mathlib.RingTheory.Noetherian.Basic
{R₁ : Type u_5} {S : Type u_6} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] [IsNoetherian R₁ S] (I : Ideal S) : Module.Finite R₁ ↥I
Module.Finite.of_injective 📋 Mathlib.RingTheory.Noetherian.Basic
{R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] [IsNoetherian S N] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (f : M →ₛₗ[σ] N) (hf : Function.Injective ⇑f) : Module.Finite R M
IsNoetherianRing.of_finite 📋 Mathlib.RingTheory.Noetherian.Basic
(R : Type u_1) (S : Type u_2) [Ring R] [Ring S] [Module R S] [IsScalarTower R S S] [IsNoetherianRing R] [Module.Finite R S] : IsNoetherianRing S
isNoetherian_linearMap 📋 Mathlib.RingTheory.Noetherian.Basic
(R : Type u_1) (M : Type u_2) (N : Type u_3) [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [IsNoetherian R M] [Module.Finite R N] : IsNoetherian R (N →ₗ[R] M)
Module.exists_finite_presentation 📋 Mathlib.RingTheory.Noetherian.Basic
(R : Type u) [CommRing R] [Small.{v, u} R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ P x x_1, ∃ (_ : Module.Free R P) (_ : Module.Finite R P), ∃ f, Function.Surjective ⇑f
OrzechProperty.bijective_of_surjective_endomorphism 📋 Mathlib.RingTheory.OrzechProperty
{R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] (f : M →ₗ[R] M) (hf : Function.Surjective ⇑f) : Function.Bijective ⇑f
OrzechProperty.injective_of_surjective_endomorphism 📋 Mathlib.RingTheory.OrzechProperty
{R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] (f : M →ₗ[R] M) (hf : Function.Surjective ⇑f) : Function.Injective ⇑f
OrzechProperty.bijective_of_surjective_of_injective 📋 Mathlib.RingTheory.OrzechProperty
{R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] {N : Type w} [AddCommMonoid N] [Module R N] (i f : N →ₗ[R] M) (hi : Function.Injective ⇑i) (hf : Function.Surjective ⇑f) : Function.Bijective ⇑f
OrzechProperty.injective_of_surjective_of_injective 📋 Mathlib.RingTheory.OrzechProperty
{R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] {N : Type w} [AddCommMonoid N] [Module R N] (i f : N →ₗ[R] M) (hi : Function.Injective ⇑i) (hf : Function.Surjective ⇑f) : Function.Injective ⇑f
OrzechProperty.injective_of_surjective_of_submodule 📋 Mathlib.RingTheory.OrzechProperty
{R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M) (hf : Function.Surjective ⇑f) : Function.Injective ⇑f
OrzechProperty.injective_of_surjective_of_submodule' 📋 Mathlib.RingTheory.OrzechProperty
{R : Type u} {inst✝ : Semiring R} [self : OrzechProperty R] {M : Type u} [AddCommMonoid M] [Module R M] [Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M) : Function.Surjective ⇑f → Function.Injective ⇑f
OrzechProperty.mk 📋 Mathlib.RingTheory.OrzechProperty
{R : Type u} [Semiring R] (injective_of_surjective_of_submodule' : ∀ {M : Type u} [inst : AddCommMonoid M] [inst_1 : Module R M] [Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f) : OrzechProperty R
orzechProperty_iff 📋 Mathlib.RingTheory.OrzechProperty
(R : Type u) [Semiring R] : OrzechProperty R ↔ ∀ {M : Type u} [inst : AddCommMonoid M] [inst_1 : Module R M] [Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
Module.Finite.exists_nat_not_surjective 📋 Mathlib.LinearAlgebra.InvariantBasisNumber
(R : Type u) [Semiring R] [RankCondition R] (M : Type u_1) [AddCommMonoid M] [Module R M] [Module.Finite R M] : ∃ n, ∀ (f : M →ₗ[R] Fin n → R), ¬Function.Surjective ⇑f
Module.rank_lt_aleph0 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] : Module.rank R M < Cardinal.aleph0
Module.finrank_eq_rank 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] : ↑(Module.finrank R M) = Module.rank R M
Module.mk_finrank_eq_card_basis 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type w} (h : Module.Basis ι R M) : ↑(Module.finrank R M) = Cardinal.mk ι
Module.finrank_eq_zero_iff_of_free 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Free R M] [Module.Finite R M] : Module.finrank R M = 0 ↔ Subsingleton M
Module.finrank_pos_iff_of_free 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Free R M] [Module.Finite R M] : 0 < Module.finrank R M ↔ Nontrivial M
LinearMap.finrank_le_finrank_of_injective 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {M' : Type u_2} [AddCommMonoid M'] [Module R M'] [Module.Finite R M'] {f : M →ₗ[R] M'} (hf : Function.Injective ⇑f) : Module.finrank R M ≤ Module.finrank R M'
LinearMap.finrank_le_finrank_of_surjective 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {M' : Type u_2} [AddCommMonoid M'] [Module R M'] [Module.Finite R M] {f : M →ₗ[R] M'} (hf : Function.Surjective ⇑f) : Module.finrank R M' ≤ Module.finrank R M
Submodule.finrank_eq_rank 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M) : ↑(Module.finrank R ↥N) = Module.rank R ↥N
LinearMap.finrank_range_le 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {M' : Type u_2} [AddCommMonoid M'] [Module R M'] [Module.Finite R M] (f : M →ₗ[R] M') : Module.finrank R ↥f.range ≤ Module.finrank R M
Module.instFintypeElemExtendOfFiniteSubtypeMemSubmoduleSpan 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
{R : Type u_2} {M : Type u_3} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set M} [Module.Finite R ↥(Submodule.span R t)] (hs : LinearIndepOn R id s) (hst : s ⊆ t) : Fintype ↑(hs.extend hst)
Submodule.exists_finset_span_eq_linearIndepOn 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(K : Type u_2) {M : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] (s : Set M) [Module.Finite K ↥(Submodule.span K s)] : ∃ t, ↑t ⊆ s ∧ t.card = Module.finrank K ↥(Submodule.span K s) ∧ Submodule.span K ↑t = Submodule.span K s ∧ LinearIndepOn K id ↑t
Module.finrank_top_le_finrank_of_isScalarTower 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(R : Type u) (S : Type u_1) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [Semiring S] [Module S M] [Module R S] [IsScalarTower R S S] [FaithfulSMul R S] [IsScalarTower R S M] : Module.finrank S M ≤ Module.finrank R M
LinearMap.finrank_le_of_isSMulRegular 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {S : Type u_2} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (L L' : Submodule R M) [Module.Finite R ↥L'] {s : S} (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') : Module.finrank R ↥L ≤ Module.finrank R ↥L'
Module.finrank_bot_le_finrank_of_isScalarTower 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(R : Type u) [Semiring R] [StrongRankCondition R] (S : Type u_2) (T : Type u_3) [Semiring S] [Semiring T] [Module R T] [Module S T] [Module R S] [IsScalarTower R S T] [IsScalarTower S T T] [FaithfulSMul S T] [Module.Finite R T] : Module.finrank R S ≤ Module.finrank R T
Submodule.mem_span_set_iff_exists_finsupp_le_finrank 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
{K : Type u_2} {M : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] {s : Set M} {x : M} [Module.Finite K ↥(Submodule.span K s)] : x ∈ Submodule.span K s ↔ ∃ c, c.support.card ≤ Module.finrank K ↥(Submodule.span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = x
Submodule.exists_fun_fin_finrank_span_eq 📋 Mathlib.LinearAlgebra.Dimension.StrongRankCondition
(K : Type u_2) {M : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] (s : Set M) [Module.Finite K ↥(Submodule.span K s)] : ∃ f, (∀ (i : Fin (Module.finrank K ↥(Submodule.span K s))), f i ∈ s) ∧ Submodule.span K (Set.range f) = Submodule.span K s ∧ LinearIndependent K f
Module.Finite.of_basis 📋 Mathlib.LinearAlgebra.FreeModule.Finite.Basic
{R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Module.Basis ι R M) : Module.Finite R M
Module.Free.ChooseBasisIndex.fintype 📋 Mathlib.LinearAlgebra.FreeModule.Finite.Basic
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] : Fintype (Module.Free.ChooseBasisIndex R M)
Module.Finite.matrix 📋 Mathlib.LinearAlgebra.FreeModule.Finite.Basic
{R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [Finite ι₁] [Finite ι₂] : Module.Finite R (Matrix ι₁ ι₂ M)
Module.finite_of_finrank_eq_succ 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] {n : ℕ} (hn : Module.finrank R M = n.succ) : Module.Finite R M
Algebra.instFiniteOfIsQuadraticExtension 📋 Mathlib.LinearAlgebra.Dimension.Free
(R : Type u_2) (S : Type u_3) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S] [Algebra.IsQuadraticExtension R S] : Module.Finite R S
Module.finBasis 📋 Mathlib.LinearAlgebra.Dimension.Free
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] [Module.Finite R M] : Module.Basis (Fin (Module.finrank R M)) R M
Module.finite_of_finrank_pos 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] (h : 0 < Module.finrank R M) : Module.Finite R M
Module.finrank_of_not_finite 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] (h : ¬Module.Finite R M) : Module.finrank R M = 0
Module.rank_lt_aleph0_iff 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] : Module.rank R M < Cardinal.aleph0 ↔ Module.Finite R M
Module.finBasisOfFinrankEq 📋 Mathlib.LinearAlgebra.Dimension.Free
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] [Module.Finite R M] {n : ℕ} (hn : Module.finrank R M = n) : Module.Basis (Fin n) R M
Module.finrank_eq_card_chooseBasisIndex 📋 Mathlib.LinearAlgebra.Dimension.Free
(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] [Module.Finite R M] : Module.finrank R M = Fintype.card (Module.Free.ChooseBasisIndex R M)
LinearEquiv.ofFinrankEq 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} (M : Type v) (M' : Type v') [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [AddCommMonoid M'] [Module R M'] [Module.Free R M'] [StrongRankCondition R] [Module.Finite R M] [Module.Finite R M'] (cond : Module.finrank R M = Module.finrank R M') : M ≃ₗ[R] M'
FiniteDimensional.nonempty_linearEquiv_of_finrank_eq 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [AddCommMonoid M'] [Module R M'] [Module.Free R M'] [StrongRankCondition R] [Module.Finite R M] [Module.Finite R M'] (cond : Module.finrank R M = Module.finrank R M') : Nonempty (M ≃ₗ[R] M')
FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [AddCommMonoid M'] [Module R M'] [Module.Free R M'] [StrongRankCondition R] [Module.Finite R M] [Module.Finite R M'] : Nonempty (M ≃ₗ[R] M') ↔ Module.finrank R M = Module.finrank R M'
Module.finite_iff_of_rank_eq_nsmul 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] {W : Type v} [AddCommMonoid W] [Module R W] [Module.Free R W] {n : ℕ} (hn : n ≠ 0) (hVW : Module.rank R M = n • Module.rank R W) : Module.Finite R M ↔ Module.Finite R W
finrank_le_iff_exists_linearMap 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [AddCommMonoid M'] [Module R M'] [Module.Free R M'] [StrongRankCondition R] [Module.Finite R M] [Module.Finite R M'] : Module.finrank R M ≤ Module.finrank R M' ↔ ∃ f, Function.Injective ⇑f
OrzechProperty.bijective_of_surjective_of_finrank_le 📋 Mathlib.LinearAlgebra.Dimension.Free
{R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [AddCommMonoid M'] [Module R M'] [Module.Free R M'] [OrzechProperty R] [Module.Finite R M] [Module.Finite R M'] (f : M →ₗ[R] M') (hf : Function.Surjective ⇑f) (h : Module.finrank R M ≤ Module.finrank R M') : Function.Bijective ⇑f
Module.finrank_div_finrank_cancel_right_of_nontrivial 📋 Mathlib.LinearAlgebra.Dimension.Free
(F : Type u) (K : Type v) (A : Type w) [Semiring F] [Semiring K] [AddCommMonoid A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] [Module.Free K A] [Nontrivial A] [Module.Finite K A] : Module.finrank F A / Module.finrank K A = Module.finrank F K
Module.finrank_div_finrank_cancel_left_of_nontrivial 📋 Mathlib.LinearAlgebra.Dimension.Free
(F : Type u) (K : Type v) (A : Type w) [Semiring F] [Semiring K] [AddCommMonoid A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] [Module.Free K A] [Nontrivial K] [Module.Finite F K] : Module.finrank F A / Module.finrank F K = Module.finrank K A
Module.finrank_top_le_finrank_of_isScalarTower_of_free 📋 Mathlib.LinearAlgebra.Dimension.Free
(R : Type u) (S : Type u_1) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Semiring S] [StrongRankCondition S] [Module S M] [Module R S] [FaithfulSMul R S] [Module.Finite R S] [IsScalarTower R S S] [IsScalarTower R S M] [Module.Free S M] : Module.finrank S M ≤ Module.finrank R M
Module.finrank_bot_le_finrank_of_isScalarTower_of_free 📋 Mathlib.LinearAlgebra.Dimension.Free
(R : Type u) [Semiring R] [StrongRankCondition R] (S : Type u_2) (T : Type u_3) [Semiring S] [Semiring T] [Module R T] [Module S T] [Module R S] [IsScalarTower R S T] [IsScalarTower S T T] [FaithfulSMul S T] [Module.Finite S T] [Module.Free R S] : Module.finrank R S ≤ Module.finrank R T
Module.free_of_finite_type_torsion_free' 📋 Mathlib.LinearAlgebra.FreeModule.PID
{R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsPrincipalIdealRing R] [IsDomain R] [Module.Finite R M] [Module.IsTorsionFree R M] : Module.Free R M
Module.free_iff_isTorsionFree 📋 Mathlib.LinearAlgebra.FreeModule.PID
{R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsPrincipalIdealRing R] [IsDomain R] [Module.Finite R M] : Module.Free R M ↔ Module.IsTorsionFree R M
Module.basisOfFiniteTypeTorsionFree' 📋 Mathlib.LinearAlgebra.FreeModule.PID
{R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsPrincipalIdealRing R] [IsDomain R] [Module.Finite R M] [Module.IsTorsionFree R M] : (n : ℕ) × Module.Basis (Fin n) R M
instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree 📋 Mathlib.LinearAlgebra.FreeModule.PID
{R : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [IsDomain R] {S : Type u_4} [CommRing S] [Algebra R S] {I : Ideal S} [hI₁ : Module.Finite R ↥I] [hI₂ : Module.IsTorsionFree R ↥I] : Module.Free R ↥I
instNontrivialTensorProduct 📋 Mathlib.RingTheory.TensorProduct.Finite
(R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : Nontrivial (TensorProduct R M M)
Module.Finite.tensorProduct 📋 Mathlib.RingTheory.TensorProduct.Finite
(R : Type u_1) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [hM : Module.Finite R M] [hN : Module.Finite R N] : Module.Finite R (TensorProduct R M N)
Module.Finite.base_change 📋 Mathlib.RingTheory.TensorProduct.Finite
(R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [h : Module.Finite R M] : Module.Finite A (TensorProduct R A M)
Module.exists_isPrincipal_quotient_of_finite 📋 Mathlib.RingTheory.TensorProduct.Finite
(R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : ∃ N, N ≠ ⊤ ∧ ⊤.IsPrincipal
Module.exists_surjective_quotient_of_finite 📋 Mathlib.RingTheory.TensorProduct.Finite
(R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : ∃ I f, I ≠ ⊤ ∧ Function.Surjective ⇑f
Subalgebra.finite_sup 📋 Mathlib.RingTheory.TensorProduct.Finite
{K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] [Algebra K L] (E1 E2 : Subalgebra K L) [Module.Finite K ↥E1] [Module.Finite K ↥E2] : Module.Finite K ↥(E1 ⊔ E2)
Algebra.isEpi_iff_surjective_algebraMap_of_finite 📋 Mathlib.Algebra.Algebra.Epi
{R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Module.Finite R A] : Algebra.IsEpi R A ↔ Function.Surjective ⇑(algebraMap R A)
Module.finrank_pi_fintype 📋 Mathlib.LinearAlgebra.Dimension.Constructions
(R : Type u) [Semiring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] [∀ (i : ι), Module.Finite R (M i)] : Module.finrank R ((i : ι) → M i) = ∑ i, Module.finrank R (M i)
Submodule.finrank_le 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] (s : Submodule R M) : Module.finrank R ↥s ≤ Module.finrank R M
Module.finrank_directSum 📋 Mathlib.LinearAlgebra.Dimension.Constructions
(R : Type u) [Semiring R] [StrongRankCondition R] {ι : Type v} [Fintype ι] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] [∀ (i : ι), Module.Finite R (M i)] : Module.finrank R (DirectSum ι fun i => M i) = ∑ i, Module.finrank R (M i)
Module.finrank_prod 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] [StrongRankCondition R] [Module.Free R M] [Module.Free R M'] [Module.Finite R M] [Module.Finite R M'] : Module.finrank R (M × M') = Module.finrank R M + Module.finrank R M'
Submodule.finrank_quotient_le 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] (s : Submodule R M) : Module.finrank R (M ⧸ s) ≤ Module.finrank R M
Submodule.finrank_mono 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {s t : Submodule R M} [Module.Finite R ↥t] (hst : s ≤ t) : Module.finrank R ↥s ≤ Module.finrank R ↥t
Submodule.finrank_map_le 📋 Mathlib.LinearAlgebra.Dimension.Constructions
{R : Type u} {M : Type v} {M' : Type v'} [Semiring R] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [StrongRankCondition R] [Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) [Module.Finite R ↥p] : Module.finrank R ↥(Submodule.map f p) ≤ Module.finrank R ↥p
LinearIndependent.finite 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type u_1} {f : ι → M} (h : LinearIndependent R f) : Finite ι
Module.Finite.not_linearIndependent_of_infinite 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [StrongRankCondition R] {ι : Type u_1} [Infinite ι] (v : ι → M) : ¬LinearIndependent R v
Module.finite_of_rank_eq_nat 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] {n : ℕ} (h : Module.rank R M = ↑n) : Module.Finite R M
Module.finite_of_rank_eq_one 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] (h : Module.rank R M = 1) : Module.Finite R M
Module.finite_finsupp_self_iff 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} [Semiring R] {ι : Type u_1} : Module.Finite R (ι →₀ R) ↔ Subsingleton R ∨ Finite ι
LinearIndependent.lt_aleph0_of_finite 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] {ι : Type w} [Module.Finite R M] {v : ι → M} (h : LinearIndependent R v) : Cardinal.mk ι < Cardinal.aleph0
LinearIndependent.cardinalMk_le_finrank 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type w} {b : ι → M} (h : LinearIndependent R b) : Cardinal.mk ι ≤ ↑(Module.finrank R M)
LinearIndependent.fintype_card_le_finrank 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {ι : Type u_1} [Fintype ι] {b : ι → M} (h : LinearIndependent R b) : Fintype.card ι ≤ Module.finrank R M
LinearIndependent.setFinite 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {b : Set M} (h : LinearIndependent R fun (x : ↑b) => ↑x) : b.Finite
Module.finite_finsupp_iff 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_1} : Module.Finite R (ι →₀ M) ↔ IsEmpty ι ∨ Subsingleton M ∨ Module.Finite R M ∧ Finite ι
Module.finite_of_rank_eq_zero 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] (h : Module.rank R M = 0) : Module.Finite R M
Module.finrank_pos 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M] [h : Nontrivial M] : 0 < Module.finrank R M
Module.finrank_zero_iff 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M] : Module.finrank R M = 0 ↔ Subsingleton M
Module.finrank_pos_iff 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M] : 0 < Module.finrank R M ↔ Nontrivial M
LinearIndependent.finset_card_le_finrank 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Finite R M] {b : Finset M} (h : LinearIndependent R fun x => ↑x) : b.card ≤ Module.finrank R M
Module.finrank_pos_iff_exists_ne_zero 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M] : 0 < Module.finrank R M ↔ ∃ x, x ≠ 0
iSupIndep.fintypeNeBotOfFiniteDimensional 📋 Mathlib.LinearAlgebra.Dimension.Finite
{ι : Type w} {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] [Module.Finite R M] [StrongRankCondition R] {p : ι → Submodule R M} (hp : iSupIndep p) : Fintype { i // p i ≠ ⊥ }
iSupIndep.subtype_ne_bot_le_finrank_aux 📋 Mathlib.LinearAlgebra.Dimension.Finite
{ι : Type w} {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] [Module.Finite R M] [StrongRankCondition R] {p : ι → Submodule R M} (hp : iSupIndep p) : Cardinal.mk { i // p i ≠ ⊥ } ≤ ↑(Module.finrank R M)
Module.finrank_eq_zero_iff 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] : Module.finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
Module.finrank_quotient_add_finrank_le 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M) : Module.finrank R (M ⧸ N) + Module.finrank R ↥N ≤ Module.finrank R M
iSupIndep.subtype_ne_bot_le_finrank 📋 Mathlib.LinearAlgebra.Dimension.Finite
{ι : Type w} {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] [Module.Finite R M] [StrongRankCondition R] {p : ι → Submodule R M} (hp : iSupIndep p) [Fintype { i // p i ≠ ⊥ }] : Fintype.card { i // p i ≠ ⊥ } ≤ Module.finrank R M
Module.exists_nontrivial_relation_of_finrank_lt_card 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] [StrongRankCondition R] {t : Finset M} (h : Module.finrank R M < t.card) : ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0
Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] [StrongRankCondition R] {t : Finset M} (h : Module.finrank R M + 1 < t.card) : ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
Submodule.finrank_eq_zero 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] [StrongRankCondition R] {S : Submodule R M} [Module.Finite R ↥S] : Module.finrank R ↥S = 0 ↔ S = ⊥
Submodule.one_le_finrank_iff 📋 Mathlib.LinearAlgebra.Dimension.Finite
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] [StrongRankCondition R] {S : Submodule R M} [Module.Finite R ↥S] : 1 ≤ Module.finrank R ↥S ↔ S ≠ ⊥
Submodule.finite_iSup 📋 Mathlib.RingTheory.Finiteness.Lattice
{R : Type u_2} {V : Type u_3} [Ring R] [AddCommGroup V] [Module R V] {ι : Sort u_1} [Finite ι] (S : ι → Submodule R V) [∀ (i : ι), Module.Finite R ↥(S i)] : Module.Finite R ↥(⨆ i, S i)
IsField.of_isDomain_of_finite 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
(K : Type u_1) (L : Type u_2) [Field K] [CommRing L] [IsDomain L] [Algebra K L] [Module.Finite K L] : IsField L
LinearMap.instIsStablyFiniteRingEnd 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
(R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [IsStablyFiniteRing R] : IsStablyFiniteRing (Module.End R M)
Module.End.injective_of_surjective 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
(R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [IsStablyFiniteRing R] {f : Module.End R M} (hf : Function.Surjective ⇑f) : Function.Injective ⇑f
LinearMap.comp_eq_id_comm 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
(R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [IsStablyFiniteRing R] {f g : M →ₗ[R] M} : f ∘ₗ g = LinearMap.id ↔ g ∘ₗ f = LinearMap.id
cardinal_lt_aleph0_of_finiteDimensional 📋 Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
(K : Type u) (V : Type v) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Finite K] [Module.Free K V] [Module.Finite K V] : Cardinal.mk V < Cardinal.aleph0
cardinalMk_eq_cardinalMk_field_pow_rank 📋 Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
(K V : Type u) [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] : Cardinal.mk V = Cardinal.mk K ^ Module.rank K V
lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank 📋 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] : Cardinal.lift.{u, v} (Cardinal.mk V) = Cardinal.lift.{v, u} (Cardinal.mk K) ^ Cardinal.lift.{u, v} (Module.rank K V)
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
finrank_le_one_iff 📋 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 ↔ ∃ v, ∀ (w : V), ∃ c, c • v = w
Submodule.finrank_le_one_iff_isPrincipal 📋 Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
{K : Type u} {V : Type v} [Ring K] [StrongRankCondition K] [AddCommGroup V] [Module K V] (W : Submodule K V) [Module.Free K ↥W] [Module.Finite K ↥W] : Module.finrank K ↥W ≤ 1 ↔ W.IsPrincipal
Polynomial.not_finite 📋 Mathlib.RingTheory.Polynomial.Basic
{R : Type u} [Semiring R] [Nontrivial R] : ¬Module.Finite R (Polynomial R)
MvPolynomial.instFiniteOfIsEmpty 📋 Mathlib.RingTheory.Polynomial.Basic
{ι : Type u_2} {R : Type u_3} [CommSemiring R] [IsEmpty ι] : Module.Finite R (MvPolynomial ι R)
Module.Finite.finiteType 📋 Mathlib.RingTheory.FiniteType
{R : Type u_1} (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [hRA : Module.Finite R A] : Algebra.FiniteType R A
IsAzumaya.toFinite 📋 Mathlib.Algebra.Azumaya.Defs
{R : Type u_1} {A : Type u_2} {inst✝ : CommSemiring R} {inst✝¹ : Semiring A} {inst✝² : Algebra R A} [self : IsAzumaya R A] : Module.Finite R A
IsAzumaya.mk 📋 Mathlib.Algebra.Azumaya.Defs
{R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [toProjective : Module.Projective R A] [toFaithfulSMul : FaithfulSMul R A] [toFinite : Module.Finite R A] (bij : Function.Bijective ⇑(AlgHom.mulLeftRight R A)) : IsAzumaya R A
MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite 📋 Mathlib.RingTheory.MvPolynomial.Basic
(σ : Type u) (R : Type v) [CommSemiring R] [Finite σ] (N : ℕ) : Module.Finite R ↥(MvPolynomial.restrictDegree σ R N)
MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite 📋 Mathlib.RingTheory.MvPolynomial.Basic
(σ : Type u) (R : Type v) [CommSemiring R] [Finite σ] (N : ℕ) : Module.Finite R ↥(MvPolynomial.restrictTotalDegree σ R N)
Module.Finite.small 📋 Mathlib.RingTheory.Finiteness.Small
(R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Small.{u, u_1} R] [Module.Finite R M] : Small.{u, u_2} M
TensorProduct.exists_finite_submodule_left_of_setFinite 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (s : Set (TensorProduct R M N)) (hs : s.Finite) : ∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.rTensor N M'.subtype).range
TensorProduct.exists_finite_submodule_right_of_setFinite 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (s : Set (TensorProduct R M N)) (hs : s.Finite) : ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range
TensorProduct.exists_finite_submodule_of_setFinite 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (s : Set (TensorProduct R M N)) (hs : s.Finite) : ∃ M' N', Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(TensorProduct.mapIncl M' N').range
TensorProduct.exists_finite_submodule_left_of_setFinite' 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N} (s : Set (TensorProduct R ↥M₁ ↥N₁)) (hs : s.Finite) : ∃ M', ∃ (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.rTensor (↥N₁) (Submodule.inclusion hM)).range
TensorProduct.exists_finite_submodule_right_of_setFinite' 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N} (s : Set (TensorProduct R ↥M₁ ↥N₁)) (hs : s.Finite) : ∃ N', ∃ (hN : N' ≤ N₁), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor (↥M₁) (Submodule.inclusion hN)).range
TensorProduct.exists_finite_submodule_of_setFinite' 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
{R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N} (s : Set (TensorProduct R ↥M₁ ↥N₁)) (hs : s.Finite) : ∃ M' N', ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN)).range
Module.Flat.mk 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (out : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] [Module.Finite R P] (N : Submodule R P), N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)) : Module.Flat R M
Module.Flat.out 📋 Mathlib.RingTheory.Flat.Basic
{R : Type u} {M : Type v} {inst✝ : CommSemiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : Module R M} [self : Module.Flat R M] ⦃P : Type u⦄ [AddCommMonoid P] [Module R P] [Module.Finite R P] (N : Submodule R P) : N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)
Module.flat_iff 📋 Mathlib.RingTheory.Flat.Basic
(R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.Flat R M ↔ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] [Module.Finite R P] (N : Submodule R P), N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)
Submodule.finrank_quotient_add_finrank 📋 Mathlib.LinearAlgebra.Dimension.RankNullity
{R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M) : Module.finrank R (M ⧸ N) + Module.finrank R ↥N = Module.finrank R M
Submodule.exists_of_finrank_lt 📋 Mathlib.LinearAlgebra.Dimension.RankNullity
{R : Type u_1} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M) (h : Module.finrank R ↥N < Module.finrank R M) : ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
Submodule.finrank_quotient 📋 Mathlib.LinearAlgebra.Dimension.RankNullity
{R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_2} R] [StrongRankCondition R] [Module.Finite R M] {S : Type u_1} [Ring S] [SMul R S] [Module S M] [IsScalarTower R S M] (N : Submodule S M) : Module.finrank R (M ⧸ N) = Module.finrank R M - Module.finrank R ↥N
Submodule.disjoint_ker_of_finrank_le 📋 Mathlib.LinearAlgebra.Dimension.RankNullity
{R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [HasRankNullity.{u, u_2} R] [StrongRankCondition R] [IsDomain R] [Module.IsTorsionFree R M] {N : Type u_1} [AddCommGroup N] [Module R N] {L : Submodule R M} [Module.Finite R ↥L] (f : M →ₗ[R] N) (h : Module.finrank R ↥L ≤ Module.finrank R ↥(Submodule.map f L)) : Disjoint L f.ker
Submodule.eq_top_iff_finrank_eq 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [Module.Finite K V] {W : Submodule K V} : W = ⊤ ↔ Module.finrank K ↥W = Module.finrank K V
Submodule.sup_span_singleton_eq_top_iff 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [Module.Finite K V] {W : Submodule K V} {v : V} (hv : v ∉ W) : W ⊔ K ∙ v = ⊤ ↔ Module.finrank K (V ⧸ W) = 1
Submodule.finrank_sup_span_singleton 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
{K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [Module.Finite K V] {p : Submodule K V} {v : V} (hv : v ∉ p) : Module.finrank K ↥(p ⊔ K ∙ v) = Module.finrank K ↥p + 1
Module.Finite.exists_comp_eq_id_of_projective 📋 Mathlib.RingTheory.Finiteness.Projective
(R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Projective R M] : ∃ n f g, Function.Surjective ⇑f ∧ Function.Injective ⇑g ∧ f ∘ₗ g = LinearMap.id
Module.instIsReflexiveOfFiniteOfProjective 📋 Mathlib.LinearAlgebra.Dual.Lemmas
(R : Type u_1) (N : Type u_3) [CommSemiring R] [AddCommMonoid N] [Module R N] [Module.Finite R N] [Module.Projective R N] : Module.IsReflexive R N
Module.IsReflexive.of_finite_of_free 📋 Mathlib.LinearAlgebra.Dual.Lemmas
(R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Free R M] : Module.IsReflexive R M
Module.dual_finite 📋 Mathlib.LinearAlgebra.Dual.Lemmas
{R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.Finite R (Module.Dual R M)

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:

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 find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
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 ce5dd8c