Loogle!

Result

Found 109 declarations mentioning AddSubmonoid.toAddSubsemigroup.

• AddSubmonoid.toAddSubsemigroup 📋 Mathlib.Algebra.Group.Submonoid.Defs
  {M : Type u_3} [AddZeroClass M] (self : AddSubmonoid M) : AddSubsemigroup M
• AddSubmonoid.toSubsemigroup_injective 📋 Mathlib.Algebra.Group.Submonoid.Defs
  {M : Type u_1} [AddZeroClass M] : Function.Injective AddSubmonoid.toAddSubsemigroup
• AddSubmonoid.toSubsemigroup_inj 📋 Mathlib.Algebra.Group.Submonoid.Defs
  {M : Type u_1} [AddZeroClass M] {s t : AddSubmonoid M} : s.toAddSubsemigroup = t.toAddSubsemigroup ↔ s = t
• AddSubmonoid.zero_mem' 📋 Mathlib.Algebra.Group.Submonoid.Defs
  {M : Type u_3} [AddZeroClass M] (self : AddSubmonoid M) : 0 ∈ self.carrier
• AddSubmonoid.mem_carrier 📋 Mathlib.Algebra.Group.Submonoid.Defs
  {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} {x : M} : x ∈ s.carrier ↔ x ∈ s
• AddSubmonoid.mem_toSubsemigroup 📋 Mathlib.Algebra.Group.Submonoid.Defs
  {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} {x : M} : x ∈ s.toAddSubsemigroup ↔ x ∈ s
• AddSubgroup.mem_carrier 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {s : AddSubgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s
• AddSubgroup.neg_mem' 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_3} [AddGroup G] (self : AddSubgroup G) {x : G} : x ∈ self.carrier → -x ∈ self.carrier
• AddSubgroup.mk 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_3} [AddGroup G] (toAddSubmonoid : AddSubmonoid G) (neg_mem' : ∀ {x : G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier) : AddSubgroup G
• AddSubgroup.coe_set_mk 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {s : AddSubmonoid G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier) : ↑{ toAddSubmonoid := s, neg_mem' := h_neg } = ↑s
• AddSubgroup.mem_mk 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {s : AddSubmonoid G} {x : G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier) : x ∈ { toAddSubmonoid := s, neg_mem' := h_neg } ↔ x ∈ s
• AddSubgroup.mk_le_mk 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {s t : AddSubmonoid G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier) (h_neg' : ∀ {x : G}, x ∈ t.carrier → -x ∈ t.carrier) : { toAddSubmonoid := s, neg_mem' := h_neg } ≤ { toAddSubmonoid := t, neg_mem' := h_neg' } ↔ s ≤ t
• AddSubmonoid.unop_toSubsemigroup 📋 Mathlib.Algebra.Group.Submonoid.MulOpposite
  {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid Mᵃᵒᵖ) : H.unop.toAddSubsemigroup = H.unop
• AddSubmonoid.op_toSubsemigroup 📋 Mathlib.Algebra.Group.Submonoid.MulOpposite
  {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) : H.op.toAddSubsemigroup = H.op
• AddSubgroup.unop_toSubsemigroup 📋 Mathlib.Algebra.Group.Subgroup.MulOpposite
  {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) : H.unop.toAddSubsemigroup = H.unop
• AddSubgroup.op_toSubsemigroup 📋 Mathlib.Algebra.Group.Subgroup.MulOpposite
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.op.toAddSubsemigroup = H.op
• AddSubmonoid.center_toAddSubsemigroup 📋 Mathlib.GroupTheory.Submonoid.Center
  (M : Type u_1) [AddZeroClass M] : (AddSubmonoid.center M).toAddSubsemigroup = AddSubsemigroup.center M
• AddSubmonoid.centralizer_toAddSubsemigroup 📋 Mathlib.GroupTheory.Submonoid.Centralizer
  {M : Type u_1} (S : Set M) [AddMonoid M] : (AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S
• Submodule.carrier_eq_coe 📋 Mathlib.Algebra.Module.Submodule.Defs
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (s : Submodule R M) : s.carrier = ↑s
• Submodule.mem_carrier 📋 Mathlib.Algebra.Module.Submodule.Defs
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} : x ∈ p.carrier ↔ x ∈ ↑p
• Submodule.mk 📋 Mathlib.Algebra.Module.Submodule.Defs
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (toAddSubmonoid : AddSubmonoid M) (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier) : Submodule R M
• Submodule.smul_mem' 📋 Mathlib.Algebra.Module.Submodule.Defs
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (self : Submodule R M) (c : R) {x : M} : x ∈ self.carrier → c • x ∈ self.carrier
• Submodule.eta 📋 Mathlib.Algebra.Module.Submodule.Defs
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (h : ∀ (c : R) {x : M}, x ∈ p.carrier → c • x ∈ p.carrier) : { toAddSubmonoid := p.toAddSubmonoid, smul_mem' := h } = p
• Submodule.coe_set_mk 📋 Mathlib.Algebra.Module.Submodule.Defs
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : AddSubmonoid M) (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier) : ↑{ toAddSubmonoid := S, smul_mem' := h } = ↑S
• Submodule.mem_mk 📋 Mathlib.Algebra.Module.Submodule.Defs
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {S : AddSubmonoid M} {x : M} (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier) : x ∈ { toAddSubmonoid := S, smul_mem' := h } ↔ x ∈ S
• Submodule.mk_le_mk 📋 Mathlib.Algebra.Module.Submodule.Defs
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {S S' : AddSubmonoid M} (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier) (h' : ∀ (c : R) {x : M}, x ∈ S'.carrier → c • x ∈ S'.carrier) : { toAddSubmonoid := S, smul_mem' := h } ≤ { toAddSubmonoid := S', smul_mem' := h' } ↔ S ≤ S'
• Submodule.mk_eq_bot 📋 Mathlib.Algebra.Module.Submodule.Lattice
  {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (carrier : AddSubmonoid M) (smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier) : { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = ⊥ ↔ carrier = ⊥
• Submodule.mk_eq_top 📋 Mathlib.Algebra.Module.Submodule.Lattice
  {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (carrier : AddSubmonoid M) (smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier) : { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = ⊤ ↔ carrier = ⊤
• NonUnitalSubsemiring.mem_carrier 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} [NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s
• NonUnitalSubsemiring.mk 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} [NonUnitalNonAssocSemiring R] (toAddSubmonoid : AddSubmonoid R) (mul_mem' : ∀ {a b : R}, a ∈ toAddSubmonoid.carrier → b ∈ toAddSubmonoid.carrier → a * b ∈ toAddSubmonoid.carrier) : NonUnitalSubsemiring R
• NonUnitalSubsemiring.mul_mem' 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} [NonUnitalNonAssocSemiring R] (self : NonUnitalSubsemiring R) {a b : R} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• NonUnitalSubring.mk 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} [NonUnitalNonAssocRing R] (toNonUnitalSubsemiring : NonUnitalSubsemiring R) (neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier) : NonUnitalSubring R
• NonUnitalSubring.neg_mem' 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} [NonUnitalNonAssocRing R] (self : NonUnitalSubring R) {x : R} : x ∈ self.carrier → -x ∈ self.carrier
• NonUnitalSubring.coe_set_mk 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} [NonUnitalNonAssocRing R] (S : NonUnitalSubsemiring R) (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : ↑{ toNonUnitalSubsemiring := S, neg_mem' := h } = ↑S
• NonUnitalSubring.mem_mk 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} [NonUnitalNonAssocRing R] {S : NonUnitalSubsemiring R} {x : R} (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : x ∈ { toNonUnitalSubsemiring := S, neg_mem' := h } ↔ x ∈ S
• NonUnitalSubring.mk_le_mk 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} [NonUnitalNonAssocRing R] {S S' : NonUnitalSubsemiring R} (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) (h' : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier) : { toNonUnitalSubsemiring := S, neg_mem' := h } ≤ { toNonUnitalSubsemiring := S', neg_mem' := h' } ↔ S ≤ S'
• Subsemiring.coe_center 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  (R : Type u) [NonAssocSemiring R] : ↑(Subsemiring.center R) = (NonUnitalSubsemiring.center R).carrier
• Subsemiring.center_toSubmonoid 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  (R : Type u) [NonAssocSemiring R] : (Subsemiring.center R).toSubmonoid = { carrier := (NonUnitalSubsemiring.center R).carrier, mul_mem' := ⋯, one_mem' := ⋯ }
• Subsemiring.coe_matrix 📋 Mathlib.Data.Matrix.Basic
  {n : Type u_3} {R : Type u_11} [NonAssocSemiring R] [Fintype n] [DecidableEq n] (S : Subsemiring R) : ↑S.matrix = S.toAddSubmonoid.matrix.carrier
• Subring.coe_matrix 📋 Mathlib.Data.Matrix.Basic
  {n : Type u_3} {R : Type u_11} [NonAssocRing R] [Fintype n] [DecidableEq n] (S : Subring R) : ↑S.matrix = S.toAddSubmonoid.matrix.carrier
• NonUnitalSubalgebra.mem_carrier 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s : NonUnitalSubalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s
• NonUnitalSubalgebra.mk 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (toNonUnitalSubsemiring : NonUnitalSubsemiring A) (smul_mem' : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring.carrier → c • x ∈ toNonUnitalSubsemiring.carrier) : NonUnitalSubalgebra R A
• NonUnitalSubalgebra.smul_mem' 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (self : NonUnitalSubalgebra R A) (c : R) {x : A} : x ∈ self.carrier → c • x ∈ self.carrier
• Subalgebra.coe_center 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
  (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : ↑(Subalgebra.center R A) = (NonUnitalSubsemiring.center A).carrier
• Submodule.coe_toSubalgebra 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : ↑(p.toSubalgebra h_one h_mul) = p.carrier
• Submodule.toSubalgebra_toSubsemiring 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : (p.toSubalgebra h_one h_mul).toSubsemiring = { carrier := p.carrier, mul_mem' := ⋯, one_mem' := h_one, add_mem' := ⋯, zero_mem' := ⋯ }
• NonUnitalStarSubalgebra.mem_carrier 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] {s : NonUnitalStarSubalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s
• NonUnitalStarSubalgebra.mk 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (toNonUnitalSubalgebra : NonUnitalSubalgebra R A) (star_mem' : ∀ {a : A}, a ∈ toNonUnitalSubalgebra.carrier → star a ∈ toNonUnitalSubalgebra.carrier) : NonUnitalStarSubalgebra R A
• NonUnitalStarSubalgebra.star_mem' 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] (self : NonUnitalStarSubalgebra R A) {a : A} (_ha : a ∈ self.carrier) : star a ∈ self.carrier
• Subalgebra.coe_matrix 📋 Mathlib.Algebra.Algebra.Subalgebra.Matrix
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {n : Type u_3} [Fintype n] [DecidableEq n] (S : Subalgebra R A) : ↑S.matrix = S.toAddSubmonoid.matrix.carrier
• Subsemiring.coe_nonneg 📋 Mathlib.Algebra.Ring.Subsemiring.Order
  (R : Type u_1) [Semiring R] [PartialOrder R] [IsOrderedRing R] : ↑(Subsemiring.nonneg R) = (AddSubmonoid.nonneg R).carrier
• Subalgebra.coe_pi 📋 Mathlib.Algebra.Algebra.Subalgebra.Pi
  {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [CommSemiring R] [(i : ι) → Semiring (S i)] [(i : ι) → Algebra R (S i)] (s : Set ι) (t : (i : ι) → Subalgebra R (S i)) : ↑(Subalgebra.pi s t) = (Submodule.pi s fun i => Subalgebra.toSubmodule (t i)).carrier
• Subalgebra.pi_toSubsemiring 📋 Mathlib.Algebra.Algebra.Subalgebra.Pi
  {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [CommSemiring R] [(i : ι) → Semiring (S i)] [(i : ι) → Algebra R (S i)] (s : Set ι) (t : (i : ι) → Subalgebra R (S i)) : (Subalgebra.pi s t).toSubsemiring = { carrier := (Submodule.pi s fun i => Subalgebra.toSubmodule (t i)).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
• AddSubmonoid.even_toSubsemigroup 📋 Mathlib.Algebra.Group.Subgroup.Even
  {M : Type u_1} [AddCommMonoid M] : (AddSubmonoid.even M).toAddSubsemigroup = AddSubsemigroup.even M
• 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'
• 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.toSubmodule_mk 📋 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) : { toSubmodule := p, lie_mem' := h }.toSubmodule = p
• 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.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
• LieSubmodule.mem_carrier 📋 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) {x : M} : x ∈ (↑N).carrier ↔ x ∈ ↑N
• LieSubmodule.mk 📋 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] (toSubmodule : Submodule R M) (lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier) : LieSubmodule R L M
• LieSubmodule.lie_mem 📋 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] (self : LieSubmodule R L M) {x : L} {m : M} : m ∈ (↑self).carrier → ⁅x, m⁆ ∈ (↑self).carrier
• LieSubmodule.toSubmodule_mk 📋 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] (p : Submodule R M) (h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier) : ↑{ toSubmodule := p, lie_mem := h } = p
• LieSubmodule.mk_eq_bot_iff 📋 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 : Submodule R M} {h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier} : { toSubmodule := N, lie_mem := h } = ⊥ ↔ N = ⊥
• LieSubmodule.mk_eq_top_iff 📋 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 : Submodule R M} {h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier} : { toSubmodule := N, lie_mem := h } = ⊤ ↔ N = ⊤
• LieSubmodule.mem_mk_iff' 📋 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] (p : Submodule R M) (h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier) {x : M} : x ∈ { toSubmodule := p, lie_mem := h } ↔ x ∈ p
• LieSubmodule.coe_toSet_mk 📋 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] (S : Set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : M}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x : L} {m : M}, m ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, m⁆ ∈ { 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
• LieSubmodule.mem_mk_iff 📋 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] (S : Set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : M}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x : L} {m : M}, m ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, m⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier) {x : M} : x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := h₄ } ↔ x ∈ S
• LieRinehartSubalgebra.mem_carrier 📋 Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
  {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {x : L} : x ∈ L'.carrier ↔ x ∈ ↑L'
• LieRinehartSubalgebra.mk 📋 Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
  {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (toSubmodule : Submodule A L) (lie_mem' : ∀ {a b : L}, a ∈ toSubmodule.carrier → b ∈ toSubmodule.carrier → ⁅a, b⁆ ∈ toSubmodule.carrier) : LieRinehartSubalgebra A L
• LieRinehartSubalgebra.lie_mem' 📋 Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
  {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (self : LieRinehartSubalgebra A L) {a b : L} : a ∈ self.carrier → b ∈ self.carrier → ⁅a, b⁆ ∈ self.carrier
• LieRinehartSubalgebra.toSubmodule_mk 📋 Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
  {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (p : Submodule A L) (h : ∀ {a b : L}, a ∈ p.carrier → b ∈ p.carrier → ⁅a, b⁆ ∈ p.carrier) : { toSubmodule := p, lie_mem' := h }.toSubmodule = p
• LieRinehartSubalgebra.mem_mk_iff' 📋 Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
  {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (p : Submodule A L) (h : ∀ {a b : L}, a ∈ p.carrier → b ∈ p.carrier → ⁅a, b⁆ ∈ p.carrier) {x : L} : x ∈ { toSubmodule := p, lie_mem' := h } ↔ x ∈ p
• LieRinehartSubalgebra.mk_coe 📋 Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
  {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (S : Set L) (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : A) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {a b : L}, a ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → b ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅a, b⁆ ∈ { 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
• LieRinehartSubalgebra.mem_mk_iff 📋 Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
  {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (S : Set L) (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : A) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {a b : L}, a ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → b ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅a, b⁆ ∈ { 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
• ClosedSubmodule.mk 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (toSubmodule : Submodule R M) (isClosed' : IsClosed toSubmodule.carrier) : ClosedSubmodule R M
• ClosedSubmodule.isClosed' 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (self : ClosedSubmodule R M) : IsClosed (↑self).carrier
• ClosedSubmodule.carrier_eq_coe 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] (s : ClosedSubmodule R M) : (↑s).carrier = ↑s
• ClosedSubmodule.ext 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : TopologicalSpace M} {inst✝³ : Module R M} {x y : ClosedSubmodule R M} (carrier : (↑x).carrier = (↑y).carrier) : x = y
• ClosedSubmodule.ext_iff 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : TopologicalSpace M} {inst✝³ : Module R M} {x y : ClosedSubmodule R M} : x = y ↔ (↑x).carrier = (↑y).carrier
• ClosedSubmodule.mem_mk 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] {x : M} {s : Submodule R M} {hs : IsClosed s.carrier} : x ∈ { toSubmodule := s, isClosed' := hs } ↔ x ∈ s
• Submodule.closure_eq' 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousAdd M] [ContinuousConstSMul R M] {s : Submodule R M} (hs : IsClosed s.carrier) : s.closure = { toSubmodule := s, isClosed' := hs }
• ClosedSubmodule.coe_iSup 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {ι : Sort u_1} {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] (f : ι → ClosedSubmodule R N) : ↑(⨆ i, f i) = closure (⨆ i, ↑(f i)).carrier
• ClosedSubmodule.coe_sup 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {s t : ClosedSubmodule R N} : ↑(s ⊔ t) = closure (↑s ⊔ ↑t).carrier
• ClosedSubmodule.mem_iSup 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {ι : Sort u_1} {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {x : N} {f : ι → ClosedSubmodule R N} : x ∈ ⨆ i, f i ↔ x ∈ closure (⨆ i, ↑(f i)).carrier
• ClosedSubmodule.mem_sup 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {s t : ClosedSubmodule R N} {x : N} : x ∈ s ⊔ t ↔ x ∈ closure (↑s ⊔ ↑t).carrier
• ClosedSubmodule.coe_sSup 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] (S : Set (ClosedSubmodule R N)) : ↑(sSup S) = closure (⨆ s ∈ S, ↑s).carrier
• ClosedSubmodule.mem_sSup 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {N : Type u_4} [Semiring R] [AddCommMonoid N] [TopologicalSpace N] [Module R N] [ContinuousAdd N] [ContinuousConstSMul R N] {x : N} {S : Set (ClosedSubmodule R N)} : x ∈ sSup S ↔ x ∈ closure (⨆ s ∈ S, ↑s).carrier
• AddGroupCone.eq_zero_of_mem_of_neg_mem' 📋 Mathlib.Algebra.Order.Group.Cone
  {G : Type u_1} [AddCommGroup G] (self : AddGroupCone G) {a : G} : a ∈ self.carrier → -a ∈ self.carrier → a = 0
• AddGroupCone.mk 📋 Mathlib.Algebra.Order.Group.Cone
  {G : Type u_1} [AddCommGroup G] (toAddSubmonoid : AddSubmonoid G) (eq_zero_of_mem_of_neg_mem' : ∀ {a : G}, a ∈ toAddSubmonoid.carrier → -a ∈ toAddSubmonoid.carrier → a = 0) : AddGroupCone G
• NonUnitalStarSubsemiring.mk 📋 Mathlib.Algebra.Star.NonUnitalSubsemiring
  {R : Type v} [NonUnitalNonAssocSemiring R] [Star R] (toNonUnitalSubsemiring : NonUnitalSubsemiring R) (star_mem' : ∀ {a : R}, a ∈ toNonUnitalSubsemiring.carrier → star a ∈ toNonUnitalSubsemiring.carrier) : NonUnitalStarSubsemiring R
• NonUnitalStarSubsemiring.star_mem' 📋 Mathlib.Algebra.Star.NonUnitalSubsemiring
  {R : Type v} [NonUnitalNonAssocSemiring R] [Star R] (self : NonUnitalStarSubsemiring R) {a : R} (_ha : a ∈ self.carrier) : star a ∈ self.carrier
• NonUnitalStarSubsemiring.mem_carrier 📋 Mathlib.Algebra.Star.NonUnitalSubsemiring
  {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] {s : NonUnitalStarSubsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s
• OpenAddSubgroup.mk 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] (toAddSubgroup : AddSubgroup G) (isOpen' : IsOpen toAddSubgroup.carrier) : OpenAddSubgroup G
• OpenAddSubgroup.isOpen' 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] (self : OpenAddSubgroup G) : IsOpen (↑self).carrier
• OpenNormalAddSubgroup.ext 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u} {inst✝ : AddGroup G} {inst✝¹ : TopologicalSpace G} {x y : OpenNormalAddSubgroup G} (carrier : (↑x.toOpenAddSubgroup).carrier = (↑y.toOpenAddSubgroup).carrier) : x = y
• OpenNormalAddSubgroup.ext_iff 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u} {inst✝ : AddGroup G} {inst✝¹ : TopologicalSpace G} {x y : OpenNormalAddSubgroup G} : x = y ↔ (↑x.toOpenAddSubgroup).carrier = (↑y.toOpenAddSubgroup).carrier
• ClosedAddSubgroup.mk 📋 Mathlib.Topology.Algebra.Group.ClosedSubgroup
  {G : Type u} [AddGroup G] [TopologicalSpace G] (toAddSubgroup : AddSubgroup G) (isClosed' : IsClosed toAddSubgroup.carrier) : ClosedAddSubgroup G
• ClosedAddSubgroup.isClosed' 📋 Mathlib.Topology.Algebra.Group.ClosedSubgroup
  {G : Type u} [AddGroup G] [TopologicalSpace G] (self : ClosedAddSubgroup G) : IsClosed (↑self).carrier
• ClosedAddSubgroup.ext 📋 Mathlib.Topology.Algebra.Group.ClosedSubgroup
  {G : Type u} {inst✝ : AddGroup G} {inst✝¹ : TopologicalSpace G} {x y : ClosedAddSubgroup G} (carrier : (↑x).carrier = (↑y).carrier) : x = y
• ClosedAddSubgroup.ext_iff 📋 Mathlib.Topology.Algebra.Group.ClosedSubgroup
  {G : Type u} {inst✝ : AddGroup G} {inst✝¹ : TopologicalSpace G} {x y : ClosedAddSubgroup G} : x = y ↔ (↑x).carrier = (↑y).carrier
• ClosedSubmodule.mem_iff 📋 Mathlib.Analysis.InnerProductSpace.StandardSubspace
  {H : Type u_1} [NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H) {x : H} : x ∈ S ↔ x ∈ (↑S).carrier
• FiniteIndexNormalAddSubgroup.ext 📋 Mathlib.GroupTheory.FiniteIndexNormalSubgroup
  {G : Type u_1} {inst✝ : AddGroup G} {x y : FiniteIndexNormalAddSubgroup G} (carrier : x.carrier = y.carrier) : x = y
• FiniteIndexNormalAddSubgroup.ext_iff 📋 Mathlib.GroupTheory.FiniteIndexNormalSubgroup
  {G : Type u_1} {inst✝ : AddGroup G} {x y : FiniteIndexNormalAddSubgroup G} : x = y ↔ x.carrier = y.carrier
• LinearEquiv.map_eq_of_mem_fixingSubgroup 📋 Mathlib.LinearAlgebra.FixedSubmodule
  {R : Type u_1} [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] (e : V ≃ₗ[R] V) (W : Submodule R V) (he : e ∈ fixingSubgroup (V ≃ₗ[R] V) W.carrier) : Submodule.map (↑e) W = W
• Representation.invariants_eq_inter 📋 Mathlib.RepresentationTheory.Invariants
  {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : ρ.invariants.carrier = ⋂ g, Function.fixedPoints ⇑(ρ g)
• HahnSeries.cardSuppLTSubfield_carrier 📋 Mathlib.RingTheory.HahnSeries.Cardinal
  (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] [hκ : Fact (Cardinal.aleph0 < κ)] : ↑(HahnSeries.cardSuppLTSubfield Γ R κ) = (HahnSeries.cardSuppLTAddSubgroup Γ R κ).carrier

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

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

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

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