Loogle!

Result

Found 538 declarations mentioning LieSubalgebra. Of these, only the first 200 are shown.

LieSubalgebra 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Type v
instInhabitedLieSubalgebra 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Inhabited (LieSubalgebra R L)
instZeroLieSubalgebra 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Zero (LieSubalgebra R L)
LieSubalgebra.addCommMonoid 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : AddCommMonoid (LieSubalgebra R L)
LieSubalgebra.completeLattice 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : CompleteLattice (LieSubalgebra R L)
LieSubalgebra.instAdd 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Add (LieSubalgebra R L)
LieSubalgebra.instBot 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Bot (LieSubalgebra R L)
LieSubalgebra.instInfSet 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : InfSet (LieSubalgebra R L)
LieSubalgebra.instMin 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Min (LieSubalgebra R L)
LieSubalgebra.instPartialOrder 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : PartialOrder (LieSubalgebra R L)
LieSubalgebra.instPartialOrder_1 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : PartialOrder (LieSubalgebra R L)
LieSubalgebra.instTop 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Top (LieSubalgebra R L)
LieSubalgebra.instZero 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Zero (LieSubalgebra R L)
LieSubalgebra.instSetLike 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : SetLike (LieSubalgebra R L) L
LieSubalgebra.lieSpan 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (s : Set L) : LieSubalgebra R L
LieSubalgebra.instAddSubgroupClass 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : AddSubgroupClass (LieSubalgebra R L) L
LieHom.range 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) : LieSubalgebra R L₂
LieSubalgebra.coe_injective 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Injective SetLike.coe
LieSubalgebra.toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (self : LieSubalgebra R L) : Submodule R L
instCoeLieSubalgebraSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Coe (LieSubalgebra R L) (Submodule R L)
LieSubalgebra.instIsOrderedAddMonoid 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : IsOrderedAddMonoid (LieSubalgebra R L)
LieSubalgebra.span_univ 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieSubalgebra.lieSpan R L Set.univ = ⊤
LieSubalgebra.comap 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K₂ : LieSubalgebra R L₂) : LieSubalgebra R L
LieSubalgebra.map 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K : LieSubalgebra R L) : LieSubalgebra R L₂
LieSubalgebra.subset_lieSpan 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} : s ⊆ ↑(LieSubalgebra.lieSpan R L s)
LieSubalgebra.span_empty 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : LieSubalgebra.lieSpan R L ∅ = ⊥
LieSubalgebra.toSubmodule_injective 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Injective LieSubalgebra.toSubmodule
LieSubalgebra.top_coe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ↑⊤ = Set.univ
LieSubalgebra.instCanonicallyOrderedAdd 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : CanonicallyOrderedAdd (LieSubalgebra R L)
LieSubalgebra.lieRing 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : LieRing ↥L'
LieSubalgebra.lieSpan_eq 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : LieSubalgebra.lieSpan R L ↑K = K
LieSubalgebra.mem_top 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : x ∈ ⊤
LieSubalgebra.lieSpan_neg 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} : LieSubalgebra.lieSpan R L (-s) = LieSubalgebra.lieSpan R L s
LieSubalgebra.subsingleton_bot 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Subsingleton ↥⊥
LieSubalgebra.instBracketSubtypeMem 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] : Bracket (↥L') M
LieSubalgebra.lieAlgebra 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : LieAlgebra R ↥L'
LieSubalgebra.wellFoundedGT_of_noetherian 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : WellFoundedGT (LieSubalgebra R L)
LieSubalgebra.zero_mem 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : 0 ∈ L'
LieSubalgebra.sInf_glb 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set (LieSubalgebra R L)) : IsGLB S (sInf S)
LieSubalgebra.lieRingModule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] : LieRingModule (↥L') M
LieSubalgebra.lieSpan_mono 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s t : Set L} (h : s ⊆ t) : LieSubalgebra.lieSpan R L s ≤ LieSubalgebra.lieSpan R L t
LieSubalgebra.incl 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : ↥L' →ₗ⁅R⁆ L
LieSubalgebra.bot_coe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ↑⊥ = {0}
LieSubalgebra.mem_coe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} : x ∈ ↑L' ↔ x ∈ L'
LieSubalgebra.coe_set_eq 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' L₂' : LieSubalgebra R L) : ↑L₁' = ↑L₂' ↔ L₁' = L₂'
LieSubalgebra.toSubmodule_inj 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' L₂' : LieSubalgebra R L) : L₁'.toSubmodule = L₂'.toSubmodule ↔ L₁' = L₂'
LieHom.range_eq_map 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) : f.range = LieSubalgebra.map f ⊤
LieSubalgebra.map_top 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) : f.range = LieSubalgebra.map f ⊤
LieSubalgebra.gi 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : GaloisInsertion (LieSubalgebra.lieSpan R L) SetLike.coe
LieSubalgebra.mem_bot 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : x ∈ ⊥ ↔ x = 0
LieSubalgebra.lieSpan_le 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} {K : LieSubalgebra R L} : LieSubalgebra.lieSpan R L s ≤ K ↔ s ⊆ ↑K
LieSubalgebra.incl_range 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : K.incl.range = K
LieHom.coe_range 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) : ↑f.range = Set.range ⇑f
LieSubalgebra.coe_toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : ↑L'.toSubmodule = ↑L'
LieSubalgebra.ext 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' L₂' : LieSubalgebra R L) (h : ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂') : L₁' = L₂'
LieSubalgebra.ext_iff' 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' L₂' : LieSubalgebra R L) : L₁' = L₂' ↔ ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂'
LieHom.mem_range_self 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (x : L) : f x ∈ f.range
LieSubalgebra.eq_bot_iff 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : K = ⊥ ↔ ∀ x ∈ K, x = 0
LieSubalgebra.span_iUnion 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Sort u_1} (s : ι → Set L) : LieSubalgebra.lieSpan R L (⋃ i, s i) = ⨆ i, LieSubalgebra.lieSpan R L (s i)
LieSubalgebra.gc_map_comap 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] {f : L →ₗ⁅R⁆ L₂} : GaloisConnection (LieSubalgebra.map f) (LieSubalgebra.comap f)
LieSubalgebra.map_lieSpan 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) {s : Set L} : LieSubalgebra.map f (LieSubalgebra.lieSpan R L s) = LieSubalgebra.lieSpan R L₂ (⇑f '' s)
LieSubalgebra.le_def 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : K ≤ K' ↔ ↑K ⊆ ↑K'
LieSubalgebra.bot_toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ⊥.toSubmodule = ⊥
LieSubalgebra.top_toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ⊤.toSubmodule = ⊤
LieSubalgebra.coe_inf 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : ↑(K ⊓ K') = ↑K ∩ ↑K'
LieSubalgebra.span_union 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (s t : Set L) : LieSubalgebra.lieSpan R L (s ∪ t) = LieSubalgebra.lieSpan R L s ⊔ LieSubalgebra.lieSpan R L t
LieSubalgebra.subsingleton_of_bot 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Subsingleton (LieSubalgebra R ↥⊥)
LieHom.mem_range 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (x : L₂) : x ∈ f.range ↔ ∃ y, f y = x
LieSubalgebra.instIsLieTowerSubtypeMem 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] : IsLieTower (↥L') L M
LieSubalgebra.instSMulMemClass 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : SMulMemClass (LieSubalgebra R L) R L
LieSubalgebra.mem_lieSpan 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} {x : L} : x ∈ LieSubalgebra.lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
LieSubalgebra.ofLe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : LieSubalgebra R ↥K'
LieSubalgebra.mem_carrier 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} : x ∈ L'.carrier ↔ x ∈ ↑L'
LieHom.rangeRestrict 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) : L →ₗ⁅R⁆ ↥f.range
LieSubalgebra.lieModule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] [Module R M] [LieModule R L M] : LieModule R (↥L') M
LieSubalgebra.lie_mem 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x y : L} (hx : x ∈ L') (hy : y ∈ L') : ⁅x, y⁆ ∈ L'
LieSubalgebra.toSubmodule_eq_bot 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : K.toSubmodule = ⊥ ↔ K = ⊥
LieSubalgebra.toSubmodule_eq_top 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : K.toSubmodule = ⊤ ↔ K = ⊤
LieSubalgebra.add_eq_sup 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : K + K' = K ⊔ K'
LieSubalgebra.sub_mem 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x y : L} : x ∈ L' → y ∈ L' → x - y ∈ L'
LieSubalgebra.add_mem 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x y : L} : x ∈ L' → y ∈ L' → x + y ∈ L'
LieSubalgebra.mem_inf 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) (x : L) : x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
LieSubalgebra.mem_toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} : x ∈ L'.toSubmodule ↔ x ∈ L'
LieSubalgebra.inf_toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : (K ⊓ K').toSubmodule = K.toSubmodule ⊓ K'.toSubmodule
LieSubalgebra.mem_comap 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K₂ : LieSubalgebra R L₂) {x : L} : x ∈ LieSubalgebra.comap f K₂ ↔ f x ∈ K₂
LieSubalgebra.map_le_iff_le_comap 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] {f : L →ₗ⁅R⁆ L₂} {K : LieSubalgebra R L} {K' : LieSubalgebra R L₂} : LieSubalgebra.map f K ≤ K' ↔ K ≤ LieSubalgebra.comap f K'
LieSubalgebra.mem_map 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K : LieSubalgebra R L) (x : L₂) : x ∈ LieSubalgebra.map f K ↔ ∃ y ∈ K, f y = x
LieSubalgebra.coe_sInf 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set (LieSubalgebra R L)) : ↑(sInf S) = ⋂ s ∈ S, ↑s
LieEquiv.ofInjective 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Injective ⇑f) : L₁ ≃ₗ⁅R⁆ ↥f.range
LieHom.equivRangeOfInjective 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (h : Function.Injective ⇑f) : L ≃ₗ⁅R⁆ ↥f.range
LieModuleHom.restrictLie 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type w} [AddCommGroup M] [LieRingModule L M] {N : Type w₁} [AddCommGroup N] [LieRingModule L N] [Module R N] [Module R M] (f : M →ₗ⁅R,L⁆ N) (L' : LieSubalgebra R L) : M →ₗ⁅R,↥L'⁆ N
LieSubalgebra.coe_bracket_of_module 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] (x : ↥L') (m : M) : ⁅x, m⁆ = ⁅↑x, m⁆
LieSubalgebra.inclusion 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : ↥K →ₗ⁅R⁆ ↥K'
LieEquiv.ofEq 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (L₁' L₁'' : LieSubalgebra R L₁) (h : ↑L₁' = ↑L₁'') : ↥L₁' ≃ₗ⁅R⁆ ↥L₁''
LieSubalgebra.smul_mem 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (t : R) {x : L} (h : x ∈ L') : t • x ∈ L'
LieSubalgebra.coe_lieSpan_submodule_eq_iff 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {p : Submodule R L} : (LieSubalgebra.lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p
LieSubalgebra.toSubmodule_le_toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : K.toSubmodule ≤ K'.toSubmodule ↔ K ≤ K'
LieSubalgebra.disjoint_toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} : Disjoint K.toSubmodule K'.toSubmodule ↔ Disjoint K K'
LieEquiv.ofSubalgebras 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂) (e : L₁ ≃ₗ⁅R⁆ L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') : ↥L₁' ≃ₗ⁅R⁆ ↥L₂'
LieSubalgebra.ext_iff 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (x y : ↥L') : x = y ↔ ↑x = ↑y
LieSubalgebra.ofLe_eq_comap_incl 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : LieSubalgebra.ofLe h = LieSubalgebra.comap K'.incl K
LieSubalgebra.equivMapOfInjective 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K : LieSubalgebra R L) (hf : Function.Injective ⇑f) : ↥K ≃ₗ⁅R⁆ ↥(LieSubalgebra.map f K)
LieEquiv.lieSubalgebraMap 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁'' : LieSubalgebra R L₁) (e : L₁ ≃ₗ⁅R⁆ L₂) : ↥L₁'' ≃ₗ⁅R⁆ ↥(LieSubalgebra.map e.toLieHom L₁'')
LieSubalgebra.sInf_toSubmodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set (LieSubalgebra R L)) : (sInf S).toSubmodule = sInf {x | ∃ s ∈ S, s.toSubmodule = x}
LieSubalgebra.instIsArtinianSubtypeMem 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) [IsArtinian R L] : IsArtinian R ↥L'
LieSubalgebra.instIsNoetherianSubtypeMem 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) [IsNoetherian R L] : IsNoetherian R ↥L'
LieSubalgebra.lie_mem' 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (self : LieSubalgebra R L) {x y : L} : x ∈ self.carrier → y ∈ self.carrier → ⁅x, y⁆ ∈ self.carrier
LieSubalgebra.mk 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (toSubmodule : Submodule R L) (lie_mem' : ∀ {x y : L}, x ∈ toSubmodule.carrier → y ∈ toSubmodule.carrier → ⁅x, y⁆ ∈ toSubmodule.carrier) : LieSubalgebra R L
LieSubalgebra.coe_incl 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : ⇑L'.incl = Subtype.val
LieSubalgebra.comap_incl_eq_top 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : LieSubalgebra.comap K.incl K' = ⊤ ↔ K ≤ K'
LieModuleHom.coe_restrictLie 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] {N : Type w₁} [AddCommGroup N] [LieRingModule L N] [Module R N] [Module R M] (f : M →ₗ⁅R,L⁆ N) : ⇑(f.restrictLie L') = ⇑f
LieSubalgebra.incl' 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : ↥L' →ₗ⁅R,↥L'⁆ L
LieSubalgebra.instModuleSubtypeMemOfIsScalarTower 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {R₁ : Type u_1} [Semiring R₁] [SMul R₁ R] [Module R₁ L] [IsScalarTower R₁ R L] (L' : LieSubalgebra R L) : Module R₁ ↥L'
LieSubalgebra.coe_zero_iff_zero 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (x : ↥L') : ↑x = 0 ↔ x = 0
LieHom.surjective_rangeRestrict 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) : Function.Surjective ⇑f.rangeRestrict
Submodule.exists_lieSubalgebra_coe_eq_iff 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (p : Submodule R L) : (∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
LieSubalgebra.mem_map_submodule 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (K : LieSubalgebra R L) (e : L ≃ₗ⁅R⁆ L₂) (x : L₂) : x ∈ LieSubalgebra.map e.toLieHom K ↔ x ∈ Submodule.map (↑e.toLinearEquiv) K.toSubmodule
LieSubalgebra.comap_lieSpan_range_eq 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {ι : Type u_1} (f : ι → ↥K) : LieSubalgebra.comap K.incl (LieSubalgebra.lieSpan R L (Set.range (Subtype.val ∘ f))) = LieSubalgebra.lieSpan R (↥K) (Set.range f)
LieSubalgebra.mem_mk_iff' 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (p : Submodule R L) (h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, y⁆ ∈ p.carrier) {x : L} : x ∈ { toSubmodule := p, lie_mem' := h } ↔ x ∈ p
LieSubalgebra.mem_ofLe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K') : x ∈ LieSubalgebra.ofLe h ↔ ↑x ∈ K
LieSubalgebra.lieSpan_lieSpan_coe_preimage 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} : LieSubalgebra.lieSpan R (↥(LieSubalgebra.lieSpan R L s)) (Subtype.val ⁻¹' s) = ⊤
LieHom.rangeRestrict_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (x : L) : f.rangeRestrict x = ⟨f x, ⋯⟩
LieSubalgebra.coe_bracket 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (x y : ↥L') : ↑⁅x, y⁆ = ⁅↑x, ↑y⁆
LieSubalgebra.inclusion_injective 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : Function.Injective ⇑(LieSubalgebra.inclusion h)
LieSubalgebra.coe_inclusion 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K) : ↑((LieSubalgebra.inclusion h) x) = ↑x
LieEquiv.ofInjective_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Injective ⇑f) (x : L₁) : ↑((LieEquiv.ofInjective f h) x) = f x
LieSubalgebra.equivOfLe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : ↥K ≃ₗ⁅R⁆ ↥(LieSubalgebra.ofLe h)
LieSubalgebra.lieSpan_induction 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} {p : (x : L) → x ∈ LieSubalgebra.lieSpan R L s → Prop} (mem : ∀ (x : L) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : L) (hx : x ∈ LieSubalgebra.lieSpan R L s) (hy : y ∈ LieSubalgebra.lieSpan R L s), p x hx → p y hy → p (x + y) ⋯) (smul : ∀ (a : R) (x : L) (hx : x ∈ LieSubalgebra.lieSpan R L s), p x hx → p (a • x) ⋯) {x : L} (lie : ∀ (x y : L) (hx : x ∈ LieSubalgebra.lieSpan R L s) (hy : y ∈ LieSubalgebra.lieSpan R L s), p x hx → p y hy → p ⁅x, y⁆ ⋯) (hx : x ∈ LieSubalgebra.lieSpan R L s) : p x hx
LieHom.equivRangeOfInjective_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (h : Function.Injective ⇑f) (x : L) : (f.equivRangeOfInjective h) x = ⟨f x, ⋯⟩
LieSubalgebra.inclusion_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K) : (LieSubalgebra.inclusion h) x = ⟨↑x, ⋯⟩
LieEquiv.ofEq_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (L L' : LieSubalgebra R L₁) (h : ↑L = ↑L') (x : ↥L) : ↑((LieEquiv.ofEq L L' h) x) = ↑x
LieSubalgebra.coe_ofLe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : (LieSubalgebra.ofLe h).toSubmodule = (Submodule.inclusion h).range
LieEquiv.ofSubalgebras_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂) (e : L₁ ≃ₗ⁅R⁆ L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') (x : ↥L₁') : ↑((LieEquiv.ofSubalgebras L₁' L₂' e h) x) = e ↑x
LieSubalgebra.coe_incl' 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : ⇑L'.incl' = Subtype.val
LieSubalgebra.mk_coe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set L) (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x y : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → y ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, y⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier) : ↑{ carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } = S
LieSubalgebra.mem_mk_iff 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set L) (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x y : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → y ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, y⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier) {x : L} : x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } ↔ x ∈ S
LieEquiv.ofSubalgebras_symm_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂) (e : L₁ ≃ₗ⁅R⁆ L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') (x : ↥L₂') : ↑((LieEquiv.ofSubalgebras L₁' L₂' e h).symm x) = e.symm ↑x
LieEquiv.lieSubalgebraMap_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁'' : LieSubalgebra R L₁) (e : L₁ ≃ₗ⁅R⁆ L₂) (x : ↥L₁'') : ↑((LieEquiv.lieSubalgebraMap L₁'' e) x) = e ↑x
LieSubalgebra.equivMapOfInjective_toFun_coe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K : LieSubalgebra R L) (hf : Function.Injective ⇑f) (a✝ : ↑↑K.toSubmodule) : ↑((LieSubalgebra.equivMapOfInjective f K hf) a✝) = f ↑a✝
LieSubalgebra.instIsScalarTowerSubtypeMem 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {R₁ : Type u_1} [Semiring R₁] [SMul R₁ R] [Module R₁ L] [IsScalarTower R₁ R L] (L' : LieSubalgebra R L) : IsScalarTower R₁ R ↥L'
LieSubalgebra.equivMapOfInjective_invFun_coe 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K : LieSubalgebra R L) (hf : Function.Injective ⇑f) (a✝ : ↥(Submodule.map (↑f) K.toSubmodule)) : ↑((LieSubalgebra.equivMapOfInjective f K hf).invFun a✝) = Classical.choose ⋯
LieSubalgebra.instIsCentralScalarSubtypeMem 📋 Mathlib.Algebra.Lie.Subalgebra
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {R₁ : Type u_1} [Semiring R₁] [SMul R₁ R] [SMul R₁ᵐᵒᵖ R] [Module R₁ L] [Module R₁ᵐᵒᵖ L] [IsScalarTower R₁ R L] [IsScalarTower R₁ᵐᵒᵖ R L] [IsCentralScalar R₁ L] (L' : LieSubalgebra R L) : IsCentralScalar R₁ ↥L'
LieSubalgebra.equivOfLe_apply 📋 Mathlib.Algebra.Lie.Subalgebra
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K) : (LieSubalgebra.equivOfLe h) x = ⟨(LieSubalgebra.inclusion h) x, ⋯⟩
LieSubalgebra.toLieSubmodule 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : LieSubmodule R (↥K) L
LieSubalgebra.topEquiv 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ↥⊤ ≃ₗ⁅R⁆ L
LieSubmodule.restr 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] (N : LieSubmodule R L M) (H : LieSubalgebra R L) : LieSubmodule R (↥H) M
LieSubalgebra.coe_toLieSubmodule 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : ↑K.toLieSubmodule = K.toSubmodule
LieSubmodule.restr_toSubmodule 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] (N : LieSubmodule R L M) (H : LieSubalgebra R L) : ↑(N.restr H) = ↑N
LieSubalgebra.mem_toLieSubmodule 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} (x : L) : x ∈ K.toLieSubmodule ↔ x ∈ K
LieSubmodule.mem_restr 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] {N : LieSubmodule R L M} {H : LieSubalgebra R L} {m : M} : m ∈ N.restr H ↔ m ∈ N
LieSubalgebra.topEquiv_apply 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : ↥⊤) : LieSubalgebra.topEquiv x = ↑x
LieSubmodule.map_restrictLie_incl_top 📋 Mathlib.Algebra.Lie.Submodule
{R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) [LieAlgebra R L] (H : LieSubalgebra R L) : LieSubmodule.map (N.incl.restrictLie H) ⊤ = N.restr H
lieSubalgebraOfSubalgebra 📋 Mathlib.Algebra.Lie.OfAssociative
(R : Type u) [CommRing R] (A : Type v) [Ring A] [Algebra R A] (A' : Subalgebra R A) : LieSubalgebra R A
LieModule.instIsFaithfulSubtypeMemLieSubalgebra 📋 Mathlib.Algebra.Lie.OfAssociative
(R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsFaithful R L M] {L' : LieSubalgebra R L} : LieModule.IsFaithful R (↥L') M
LieSubalgebra.toEnd_mk 📋 Mathlib.Algebra.Lie.OfAssociative
(R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (K : LieSubalgebra R L) {x : L} (hx : x ∈ K) : (LieModule.toEnd R (↥K) M) ⟨x, hx⟩ = (LieModule.toEnd R L M) x
LieSubalgebra.toEnd_eq 📋 Mathlib.Algebra.Lie.OfAssociative
(R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (K : LieSubalgebra R L) {x : ↥K} : (LieModule.toEnd R (↥K) M) x = (LieModule.toEnd R L M) ↑x
LieSubalgebra.coe_ad 📋 Mathlib.Algebra.Lie.OfAssociative
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x y : ↥H) : ↑(((LieAlgebra.ad R ↥H) x) y) = ((LieAlgebra.ad R L) ↑x) ↑y
LieSubalgebra.ad_comp_incl_eq 📋 Mathlib.Algebra.Lie.OfAssociative
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (x : ↥K) : (LieAlgebra.ad R L) ↑x ∘ₗ ↑K.incl = ↑K.incl ∘ₗ (LieAlgebra.ad R ↥K) x
LieSubalgebra.coe_ad_pow 📋 Mathlib.Algebra.Lie.OfAssociative
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x y : ↥H) (n : ℕ) : ↑(((LieAlgebra.ad R ↥H) x ^ n) y) = ((LieAlgebra.ad R L) ↑x ^ n) ↑y
LieIdeal.toLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieSubalgebra R L
instCoeLieIdealLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Coe (LieIdeal R L) (LieSubalgebra R L)
LieIdeal.top_toLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : LieIdeal.toLieSubalgebra R L ⊤ = ⊤
LieIdeal.coe_toLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↑(LieIdeal.toLieSubalgebra R L I) = ↑I
LieHom.IsIdealMorphism.eq 📋 Mathlib.Algebra.Lie.Ideal
{R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} (hf : f.IsIdealMorphism) : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
LieHom.isIdealMorphism_def 📋 Mathlib.Algebra.Lie.Ideal
{R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : f.IsIdealMorphism ↔ LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
LieHom.range_eq_top 📋 Mathlib.Algebra.Lie.Ideal
{R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : f.range = ⊤ ↔ Function.Surjective ⇑f
LieIdeal.mem_toLieSubalgebra 📋 Mathlib.Algebra.Lie.Ideal
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : L) : x ∈ LieIdeal.toLieSubalgebra R L I ↔ x ∈ I
LieHom.idealRange_eq_lieSpan_range 📋 Mathlib.Algebra.Lie.Ideal
{R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : f.idealRange = LieSubmodule.lieSpan R L' ↑f.range
LieHom.range_subset_idealRange 📋 Mathlib.Algebra.Lie.Ideal
{R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') : ↑f.range ⊆ ↑f.idealRange
LieIdeal.incl_range 📋 Mathlib.Algebra.Lie.Ideal
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.range = LieIdeal.toLieSubalgebra R L I
LieSubalgebra.exists_lieIdeal_coe_eq_iff 📋 Mathlib.Algebra.Lie.Ideal
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : (∃ I, LieIdeal.toLieSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K
LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff 📋 Mathlib.Algebra.Lie.Ideal
(R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {K' : LieSubalgebra R L} (h : K ≤ K') : (∃ I, LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
LieSubalgebra.isLieAbelian_lieSpan_iff 📋 Mathlib.Algebra.Lie.Abelian
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} : IsLieAbelian ↥(LieSubalgebra.lieSpan R L s) ↔ ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad 📋 Mathlib.Algebra.Lie.AdjointAction.Basic
{R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {x : ↥K} (h : IsNilpotent ((LieAlgebra.ad R L) ↑x)) : IsNilpotent ((LieAlgebra.ad R ↥K) x)
LieAlgebra.isNilpotent_ad_of_isNilpotent 📋 Mathlib.Algebra.Lie.AdjointAction.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {L : LieSubalgebra R A} {x : ↥L} (h : IsNilpotent ↑x) : IsNilpotent ((LieAlgebra.ad R ↥L) x)
LieDerivation.ext_of_lieSpan_eq_top 📋 Mathlib.Algebra.Lie.Derivation.Basic
{R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 D2 : LieDerivation R L M} (s : Set L) (hs : LieSubalgebra.lieSpan R L s = ⊤) (h : Set.EqOn (⇑D1) (⇑D2) s) : D1 = D2
LieDerivation.eqOn_lieSpan 📋 Mathlib.Algebra.Lie.Derivation.Basic
{R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {D1 D2 : LieDerivation R L M} {s : Set L} (h : Set.EqOn (⇑D1) (⇑D2) s) : Set.EqOn ⇑D1 ⇑D2 ↑(LieSubalgebra.lieSpan R L s)
LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop 📋 Mathlib.Algebra.Lie.Solvable
(R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSolvable L] : LieAlgebra.IsSolvable ↥⊤
LieHom.isSolvable_range 📋 Mathlib.Algebra.Lie.Solvable
{R : Type u} {L : Type v} {L' : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L' →ₗ⁅R⁆ L) [LieAlgebra.IsSolvable L'] : LieAlgebra.IsSolvable ↥f.range
LieHom.quotKerEquivRange 📋 Mathlib.Algebra.Lie.Quotient
{R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') : (L ⧸ f.ker) ≃ₗ⁅R⁆ ↥f.range
LieHom.quotKerEquivRange_invFun 📋 Mathlib.Algebra.Lie.Quotient
{R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (a✝ : ↥(↑f).range) : f.quotKerEquivRange.invFun a✝ = (↑f).quotKerEquivRange.invFun a✝
LieHom.quotKerEquivRange_toFun 📋 Mathlib.Algebra.Lie.Quotient
{R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (a : L ⧸ (↑f).ker) : f.quotKerEquivRange a = (↑f).quotKerEquivRange a
LieSubalgebra.normalizer 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : LieSubalgebra R L
LieSubalgebra.le_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : H ≤ H.normalizer
LieSubalgebra.ideal_in_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} {x y : L} (hx : x ∈ H.normalizer) (hy : y ∈ H) : ⁅x, y⁆ ∈ H
LieSubalgebra.mem_normalizer_iff 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x : L) : x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
LieSubalgebra.mem_normalizer_iff' 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) (x : L) : x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H
LieSubalgebra.coe_normalizer_eq_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : ↑H.toLieSubmodule.normalizer = H.normalizer.toSubmodule
LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H K : LieSubalgebra R L} (h₁ : H ≤ K) (h₂ : K ≤ H.normalizer) : ∃ I, LieIdeal.toLieSubalgebra R (↥K) I = LieSubalgebra.ofLe h₁
LieSubalgebra.lie_mem_sup_of_mem_normalizer 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} {x y z : L} (hx : x ∈ H.normalizer) (hy : y ∈ R ∙ x ⊔ H.toSubmodule) (hz : z ∈ R ∙ x ⊔ H.toSubmodule) : ⁅y, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
LieSubalgebra.normalizer_eq_self_iff 📋 Mathlib.Algebra.Lie.Normalizer
{R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : H.normalizer = H ↔ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule) = ⊥
instIsNilpotentSubtypeMemLieSubalgebraTop 📋 Mathlib.Algebra.Lie.Nilpotent
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [h : LieRing.IsNilpotent L] : LieRing.IsNilpotent ↥⊤
LieHom.isNilpotent_range 📋 Mathlib.Algebra.Lie.Nilpotent
{R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [LieRing.IsNilpotent L] (f : L →ₗ⁅R⁆ L') : LieRing.IsNilpotent ↥f.range
LieModule.isNilpotent_of_top_iff 📋 Mathlib.Algebra.Lie.Nilpotent
{R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule.IsNilpotent (↥⊤) M ↔ LieModule.IsNilpotent L M
LieModule.isNilpotent_range_toEnd_iff 📋 Mathlib.Algebra.Lie.Nilpotent
(R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule.IsNilpotent (↥(LieModule.toEnd R L M).range) M ↔ LieModule.IsNilpotent L M
LieAlgebra.isNilpotent_range_ad_iff 📋 Mathlib.Algebra.Lie.Nilpotent
{R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : LieRing.IsNilpotent ↥(LieAlgebra.ad R L).range ↔ LieRing.IsNilpotent L
LieModule.coe_lcs_range_toEnd_eq 📋 Mathlib.Algebra.Lie.Nilpotent
(R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ℕ) : ↑(LieModule.lowerCentralSeries R (↥(LieModule.toEnd R L M).range) M k) = ↑(LieModule.lowerCentralSeries R L M k)
LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer 📋 Mathlib.Algebra.Lie.Engel
{R : Type u₁} {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} (hK₁ : LieAlgebra.IsEngelian R ↥K) (hK₂ : K < K.normalizer) : ∃ K', LieAlgebra.IsEngelian R ↥K' ∧ K < K'
LieModule.instIsTriangularizableSubtypeMemLieSubalgebra 📋 Mathlib.Algebra.Lie.Weights.Basic
(R : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (L' : LieSubalgebra R L) [LieModule.IsTriangularizable R L M] : LieModule.IsTriangularizable R (↥L') M
LieModule.coe_genWeightSpace_of_top 📋 Mathlib.Algebra.Lie.Weights.Basic
{R : Type u_2} {L : Type u_3} (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieRing.IsNilpotent L] (χ : L → R) : ↑(LieModule.genWeightSpace M (χ ∘ ⇑⊤.incl)) = ↑(LieModule.genWeightSpace 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 69fae59