Loogle!

Result

Found 67 declarations mentioning Submodule and OrderIso.

AddSubgroup.toIntSubmodule 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommGroup M] : AddSubgroup M ≃o Submodule ℤ M
AddSubmonoid.toNatSubmodule 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommMonoid M] : AddSubmonoid M ≃o Submodule ℕ M
AddSubgroup.toIntSubmodule_toAddSubgroup 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) : (AddSubgroup.toIntSubmodule S).toAddSubgroup = S
AddSubmonoid.toNatSubmodule_toAddSubmonoid 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) : (AddSubmonoid.toNatSubmodule S).toAddSubmonoid = S
Submodule.toAddSubmonoid_toNatSubmodule 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommMonoid M] (S : Submodule ℕ M) : AddSubmonoid.toNatSubmodule S.toAddSubmonoid = S
Submodule.toAddSubgroup_toIntSubmodule 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommGroup M] (S : Submodule ℤ M) : AddSubgroup.toIntSubmodule S.toAddSubgroup = S
AddSubgroup.coe_toIntSubmodule 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) : ↑(AddSubgroup.toIntSubmodule S) = ↑S
AddSubmonoid.coe_toNatSubmodule 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) : ↑(AddSubmonoid.toNatSubmodule S) = ↑S
AddSubmonoid.toNatSubmodule_symm 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommMonoid M] : ⇑AddSubmonoid.toNatSubmodule.symm = Submodule.toAddSubmonoid
AddSubgroup.toIntSubmodule_symm 📋 Mathlib.Algebra.Module.Submodule.Lattice
{M : Type u_3} [AddCommGroup M] : ⇑AddSubgroup.toIntSubmodule.symm = Submodule.toAddSubgroup
Submodule.orderIsoMapComap 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) : Submodule R M ≃o Submodule R₂ M₂
Submodule.orderIsoMapComapOfBijective 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : Function.Bijective ⇑f) : Submodule R M ≃o Submodule R₂ M₂
Submodule.orderIsoMapComap_symm_apply 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) : (Submodule.orderIsoMapComap f).symm p = Submodule.comap f p
Submodule.orderIsoMapComap_apply' 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R M) : (Submodule.orderIsoMapComap e) p = Submodule.comap e.symm p
Submodule.orderIsoMapComap_symm_apply' 📋 Mathlib.Algebra.Module.Submodule.Map
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R₂ M₂) : (Submodule.orderIsoMapComap e).symm p = Submodule.map e.symm p
Submodule.AddMonoidHom.coe_toIntLinearMap_comap 📋 Mathlib.Algebra.Module.Submodule.Map
{A : Type u_10} {A₂ : Type u_11} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂) : Submodule.comap f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.comap f s)
AddMonoidHom.coe_toIntLinearMap_map 📋 Mathlib.Algebra.Module.Submodule.Map
{A : Type u_10} {A₂ : Type u_11} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A) : Submodule.map f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s)
AddMonoidHom.coe_toIntLinearMap_ker 📋 Mathlib.Algebra.Module.Submodule.Ker
{M : Type u_12} {M₂ : Type u_13} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker
Submodule.toIntSubmodule_toAddSubgroup 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
{R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) : AddSubgroup.toIntSubmodule N.toAddSubgroup = Submodule.restrictScalars ℤ N
AddMonoidHom.coe_toIntLinearMap_range 📋 Mathlib.Algebra.Module.Submodule.Range
{M : Type u_11} {M₂ : Type u_12} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : LinearMap.range f.toIntLinearMap = AddSubgroup.toIntSubmodule f.range
Submodule.mapIic 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule R ↥p ≃o ↑(Set.Iic p)
Submodule.MapSubtype.orderIso 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule R ↥p ≃o { p' // p' ≤ p }
Submodule.MapSubtype.relIso 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule R ↥p ≃o { p' // p' ≤ p }
Submodule.coe_mapIic_apply 📋 Mathlib.Algebra.Module.Submodule.Range
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R ↥p) : ↑(p.mapIic q) = Submodule.map p.subtype q
AddSubgroup.toIntSubmodule_closure 📋 Mathlib.LinearAlgebra.Span.Basic
{M : Type u_4} [AddCommGroup M] (s : Set M) : AddSubgroup.toIntSubmodule (AddSubgroup.closure s) = Submodule.span ℤ s
AddSubmonoid.toNatSubmodule_closure 📋 Mathlib.LinearAlgebra.Span.Basic
{M : Type u_4} [AddCommMonoid M] (s : Set M) : AddSubmonoid.toNatSubmodule (AddSubmonoid.closure s) = Submodule.span ℕ s
Submodule.negOrderIso 📋 Mathlib.Algebra.Module.Submodule.Pointwise
{R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] : Submodule R M ≃o Submodule R M
Module.Basis.addSubgroupOfClosure 📋 Mathlib.LinearAlgebra.Basis.Submodule
{M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule A)
Module.Basis.addSubgroupOfClosure.congr_simp 📋 Mathlib.LinearAlgebra.Basis.Submodule
{M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b b✝ : Module.Basis ι R M) (e_b : b = b✝) (h : A = AddSubgroup.closure (Set.range ⇑b)) : Module.Basis.addSubgroupOfClosure A b h = Module.Basis.addSubgroupOfClosure A b✝ ⋯
Module.Basis.addSubgroupOfClosure.eq_1 📋 Mathlib.LinearAlgebra.Basis.Submodule
{M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) : Module.Basis.addSubgroupOfClosure A b h = (Module.Basis.restrictScalars ℤ b).map (LinearEquiv.ofEq (Submodule.span ℤ (Set.range ⇑b)) (AddSubgroup.toIntSubmodule A) ⋯)
Module.Basis.addSubgroupOfClosure_apply 📋 Mathlib.LinearAlgebra.Basis.Submodule
{M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) (i : ι) : ↑((Module.Basis.addSubgroupOfClosure A b h) i) = b i
Module.Basis.addSubgroupOfClosure_repr_apply 📋 Mathlib.LinearAlgebra.Basis.Submodule
{M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) (x : ↥A) (i : ι) : ↑(((Module.Basis.addSubgroupOfClosure A b h).repr x) i) = (b.repr ↑x) i
Submodule.comapMkQRelIso 📋 Mathlib.LinearAlgebra.Quotient.Basic
{R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Submodule R (M ⧸ p) ≃o ↑(Set.Ici p)
Module.mapEvalEquiv 📋 Mathlib.LinearAlgebra.Dual.Defs
(R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.IsReflexive R M] : Submodule R M ≃o Submodule R (Module.Dual R (Module.Dual R M))
Module.mapEvalEquiv_apply 📋 Mathlib.LinearAlgebra.Dual.Defs
(R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.IsReflexive R M] (W : Submodule R M) : (Module.mapEvalEquiv R M) W = Submodule.map (Module.Dual.eval R M) W
Module.mapEvalEquiv_symm_apply 📋 Mathlib.LinearAlgebra.Dual.Defs
(R : Type u_3) (M : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.IsReflexive R M] (W'' : Submodule R (Module.Dual R (Module.Dual R M))) : (Module.mapEvalEquiv R M).symm W'' = Submodule.comap (Module.Dual.eval R M) 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
ModuleCat.subobjectModule 📋 Mathlib.Algebra.Category.ModuleCat.Subobject
{R : Type u} [Ring R] (M : ModuleCat R) : CategoryTheory.Subobject M ≃o Submodule R ↑M
AddSubgroup.toZModSubmodule 📋 Mathlib.Algebra.Module.ZMod
(n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] : AddSubgroup M ≃o Submodule (ZMod n) M
AddSubgroup.toZModSubmodule_toAddSubgroup 📋 Mathlib.Algebra.Module.ZMod
(n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : AddSubgroup M) : ((AddSubgroup.toZModSubmodule n) S).toAddSubgroup = S
Submodule.toAddSubgroup_toZModSubmodule 📋 Mathlib.Algebra.Module.ZMod
(n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : Submodule (ZMod n) M) : (AddSubgroup.toZModSubmodule n) S.toAddSubgroup = S
AddSubgroup.coe_toZModSubmodule 📋 Mathlib.Algebra.Module.ZMod
(n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : AddSubgroup M) : ↑((AddSubgroup.toZModSubmodule n) S) = ↑S
AddSubgroup.mem_toZModSubmodule 📋 Mathlib.Algebra.Module.ZMod
(n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] {x : M} {S : AddSubgroup M} : x ∈ (AddSubgroup.toZModSubmodule n) S ↔ x ∈ S
AddSubgroup.toZModSubmodule_symm 📋 Mathlib.Algebra.Module.ZMod
(n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] : ⇑(AddSubgroup.toZModSubmodule n).symm = Submodule.toAddSubgroup
Submodule.submodule_torsionBy_orderIso 📋 Mathlib.Algebra.Module.Torsion
{R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (a : R) : Submodule (R ⧸ Submodule.span R {a}) ↥(Submodule.torsionBy R M a) ≃o Submodule R ↥(Submodule.torsionBy R M a)
Submodule.orderIsoMapComap.congr_simp 📋 Mathlib.Algebra.Polynomial.Module.AEval
{R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ σ₁₂✝ : R →+* R₂} (e_σ₁₂ : σ₁₂ = σ₁₂✝) [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f f✝ : F) (e_f : f = f✝) : Submodule.orderIsoMapComap f = Submodule.orderIsoMapComap f✝
Module.AEval.mapSubmodule 📋 Mathlib.Algebra.Polynomial.Module.AEval
(R : Type u_1) {A : Type u_2} (M : Type u_3) [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : ↥((Algebra.lsmul R R M) a).invtSubmodule ≃o Submodule (Polynomial R) (Module.AEval R M a)
Module.AEval.mem_mapSubmodule_apply 📋 Mathlib.Algebra.Polynomial.Module.AEval
(R : Type u_2) {A : Type u_3} (M : Type u_1) [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {p : ↥((Algebra.lsmul R R M) a).invtSubmodule} {m : Module.AEval R M a} : m ∈ (Module.AEval.mapSubmodule R M a) p ↔ (Module.AEval.of R M a).symm m ∈ ↑p
Module.AEval.mem_mapSubmodule_symm_apply 📋 Mathlib.Algebra.Polynomial.Module.AEval
(R : Type u_1) {A : Type u_3} (M : Type u_2) [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {q : Submodule (Polynomial R) (Module.AEval R M a)} {m : M} : m ∈ ↑((Module.AEval.mapSubmodule R M a).symm q) ↔ (Module.AEval.of R M a) m ∈ q
Module.AEval.equiv_mapSubmodule 📋 Mathlib.Algebra.Polynomial.Module.AEval
{R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (p : Submodule R M) (hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule) : ↥p ≃ₗ[R] ↥((Module.AEval.mapSubmodule R M a) ⟨p, hp⟩)
Module.AEval.restrict_equiv_mapSubmodule 📋 Mathlib.Algebra.Polynomial.Module.AEval
{R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (p : Submodule R M) (hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule) : Module.AEval R (↥p) (LinearMap.restrict ((Algebra.lsmul R R M) a) hp) ≃ₗ[Polynomial R] ↥((Module.AEval.mapSubmodule R M a) ⟨p, hp⟩)
Module.AEval.equiv_mapSubmodule.eq_1 📋 Mathlib.Algebra.Polynomial.Module.AEval
{R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (p : Submodule R M) (hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule) : Module.AEval.equiv_mapSubmodule a p hp = { toFun := fun x => ⟨(Module.AEval.of R M a) ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, invFun := fun x => ⟨(Module.AEval.of R M a).symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
exteriorPower.ιMulti_family.eq_1 📋 Mathlib.LinearAlgebra.ExteriorPower.Basic
(R : Type u) [CommRing R] (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module R M] {I : Type u_4} [LinearOrder I] (v : I → M) (s : { s // s.card = n }) : exteriorPower.ιMulti_family R n v s = (exteriorPower.ιMulti R n) fun i => v ↑(((↑s).orderIsoOfFin ⋯) i)
IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (a✝ : ↑(Set.Iic { asIdeal := I, isPrime := hI })) : ↑((RelIso.symm (IsLocalization.AtPrime.primeSpectrumOrderIso S I)) a✝).asIdeal = ⋂ s, ⋂ (_ : ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm ⟨(↑a✝).asIdeal, ⋯⟩) ⊆ ⇑(algebraMap R S) ⁻¹' ↑s), ↑s
IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe 📋 Mathlib.RingTheory.Localization.AtPrime.Basic
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I] (a✝ : { p // p.IsPrime ∧ p ≤ I }) : ↑↑((RelIso.symm (IsLocalization.AtPrime.orderIsoOfPrime S I)) a✝) = ⋂ s, ⋂ (_ : ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm a✝) ⊆ ⇑(algebraMap R S) ⁻¹' ↑s), ↑s
Representation.mapSubmodule 📋 Mathlib.RepresentationTheory.Submodule
{k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ↥ρ.invtSubmodule ≃o Submodule (MonoidAlgebra k G) ρ.asModule
AddSubgroup.relIndex_eq_natAbs_det 📋 Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
{E : Type u_1} [AddCommGroup E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type u_2} [DecidableEq ι] [Fintype ι] (b₁ : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule L₁)) (b₂ : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule L₂)) : L₁.relIndex L₂ = (b₂.det fun i => ⟨↑(b₁ i), ⋯⟩).natAbs
AddSubgroup.relindex_eq_natAbs_det 📋 Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
{E : Type u_1} [AddCommGroup E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type u_2} [DecidableEq ι] [Fintype ι] (b₁ : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule L₁)) (b₂ : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule L₂)) : L₁.relIndex L₂ = (b₂.det fun i => ⟨↑(b₁ i), ⋯⟩).natAbs
HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk 📋 Mathlib.Algebra.Order.Module.HahnEmbedding
{K : Type u_1} [DivisionRing K] [LinearOrder K] [IsOrderedRing K] [Archimedean K] {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module K M] [IsOrderedModule K M] {R : Type u_3} [AddCommGroup R] [LinearOrder R] [Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed) [IsOrderedAddMonoid R] [Archimedean R] (x : ↥(↑f).domain) : (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x
Submodule.projectivization 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Submodule K V ≃o Projectivization.Subspace K V
Projectivization.Subspace.submodule 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Projectivization.Subspace K V ≃o Submodule K V
Projectivization.Subspace.mem_submodule_iff 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (s : Projectivization.Subspace K V) {v : V} (hv : v ≠ 0) : v ∈ Projectivization.Subspace.submodule s ↔ Projectivization.mk K v hv ∈ s
Submodule.mk_mem_projectivization_iff 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (s : Submodule K V) {v : V} (hv : v ≠ 0) : Projectivization.mk K v hv ∈ Submodule.projectivization s ↔ v ∈ s
Submodule.mem_projectivization_iff_submodule_le 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (s : Submodule K V) (x : Projectivization K V) : x ∈ Submodule.projectivization s ↔ x.submodule ≤ s
OrderIso.setIsotypicComponents 📋 Mathlib.RingTheory.SimpleModule.Isotypic
{R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : Set ↑(isotypicComponents R M) ≃o ↥(fullyInvariantSubmodule R M)
Submodule.MapSubtype.orderIso.eq_1 📋 Mathlib.RingTheory.SimpleModule.Isotypic
{R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.MapSubtype.orderIso p = { toFun := fun p' => ⟨Submodule.map p.subtype p', ⋯⟩, invFun := fun q => Submodule.comap p.subtype ↑q, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
OrderIso.setIsotypicComponents.eq_1 📋 Mathlib.RingTheory.SimpleModule.Isotypic
{R : Type u_2} {M : Type u} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : OrderIso.setIsotypicComponents = { toFun := fun s => ⨆ c ∈ s, ⟨↑c, ⋯⟩, invFun := fun m => {c | ↑c ≤ ↑m}, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

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 ?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.

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

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

Source code

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

This is Loogle revision 187ba29 serving mathlib revision c6541c0