Loogle!

Result

Found 612 declarations mentioning NonAssocRing. Of these, only the first 200 are shown.

• NonAssocRing 📋 Mathlib.Algebra.Ring.Defs
  (α : Type u_1) : Type u_1
• NonAssocCommRing.toNonAssocRing 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [self : NonAssocCommRing α] : NonAssocRing α
• NonAssocRing.toAddCommGroupWithOne 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] : AddCommGroupWithOne α
• NonAssocRing.toIntCast 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] : IntCast α
• NonAssocRing.toNatCast 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] : NatCast α
• NonAssocRing.toNonAssocSemiring 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] : NonAssocSemiring α
• NonAssocRing.toNonUnitalNonAssocRing 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] : NonUnitalNonAssocRing α
• NonAssocRing.toOne 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] : One α
• Ring.toNonAssocRing 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [Ring α] : NonAssocRing α
• IsUnital.toNonAssocRing 📋 Mathlib.Algebra.Ring.Defs
  {A : Type u_1} [NonUnitalNonAssocRing A] [IsUnital A] : NonAssocRing A
• IsMulCommutative.instNonAssocCommRing 📋 Mathlib.Algebra.Ring.Defs
  {R : Type v} [NonAssocRing R] [IsMulCommutative R] : NonAssocCommRing R
• NonAssocRing.intCast_ofNat 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] (n : ℕ) : IntCast.intCast ↑n = ↑n
• NonAssocRing.mul_one 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] (a : α) : a * 1 = a
• NonAssocRing.one_mul 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] (a : α) : 1 * a = a
• NonAssocRing.natCast_zero 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] : ↑0 = 0
• NonAssocCommRing.mk 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [toNonAssocRing : NonAssocRing α] (mul_comm : ∀ (a b : α), a * b = b * a) : NonAssocCommRing α
• NonAssocRing.intCast_negSucc 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• NonAssocRing.natCast_succ 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [self : NonAssocRing α] (n : ℕ) : ↑(n + 1) = ↑n + 1
• mul_one_sub 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [NonAssocRing α] (a b : α) : a * (1 - b) = a - a * b
• mul_sub_one 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [NonAssocRing α] (a b : α) : a * (b - 1) = a * b - a
• one_sub_mul 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [NonAssocRing α] (a b : α) : (1 - a) * b = b - a * b
• sub_one_mul 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [NonAssocRing α] (a b : α) : (a - 1) * b = a * b - b
• mul_one_sub_mul 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [NonAssocRing α] (a b c : α) : a * (1 - b) * c = a * c - a * b * c
• NonAssocRing.mk 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u_1} [toNonUnitalNonAssocRing : NonUnitalNonAssocRing α] [toOne : One α] (one_mul : ∀ (a : α), 1 * a = a) (mul_one : ∀ (a : α), a * 1 = a) [toNatCast : NatCast α] (natCast_zero : ↑0 = 0 := by intros; rfl) (natCast_succ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1 := by intros; rfl) [toIntCast : IntCast α] (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n := by intros; rfl) (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) := by intros; rfl) : NonAssocRing α
• Int.cast_mul 📋 Mathlib.Algebra.Ring.Int.Defs
  {α : Type u_1} [NonAssocRing α] (m n : ℤ) : ↑(m * n) = ↑m * ↑n
• succ_ne_self 📋 Mathlib.Algebra.Ring.Basic
  {α : Type u_3} [NonAssocRing α] [Nontrivial α] (a : α) : a + 1 ≠ a
• pred_ne_self 📋 Mathlib.Algebra.Ring.Basic
  {α : Type u_3} [NonAssocRing α] [Nontrivial α] (a : α) : a - 1 ≠ a
• RingHom.map_neg 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonAssocRing α] [NonAssocRing β] (f : α →+* β) (x : α) : f (-x) = -f x
• RingHom.map_sub 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonAssocRing α] [NonAssocRing β] (f : α →+* β) (x y : α) : f (x - y) = f x - f y
• RingHom.mk' 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocRing β] (f : α →* β) (map_add : ∀ (a b : α), f (a + b) = f a + f b) : α →+* β
• Function.Injective.nonAssocRing 📋 Mathlib.Algebra.Ring.InjSurj
  {R : Type u_1} {S : Type u_2} (f : S → R) (hf : Function.Injective f) [Add S] [Mul S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NatCast S] [IntCast S] [NonAssocRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : S), f (x + y) = f x + f y) (mul : ∀ (x y : S), f (x * y) = f x * f y) (neg : ∀ (x : S), f (-x) = -f x) (sub : ∀ (x y : S), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) : NonAssocRing S
• Function.Surjective.nonAssocRing 📋 Mathlib.Algebra.Ring.InjSurj
  {R : Type u_1} {S : Type u_2} (f : R → S) (hf : Function.Surjective f) [Add S] [Mul S] [Zero S] [One S] [Neg S] [Sub S] [SMul ℕ S] [SMul ℤ S] [NatCast S] [IntCast S] [NonAssocRing R] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) (neg : ∀ (x : R), f (-x) = -f x) (sub : ∀ (x y : R), f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x : R), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x : R), f (n • x) = n • f x) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (intCast : ∀ (n : ℤ), f ↑n = ↑n) : NonAssocRing S
• mul_self_eq_one_iff 📋 Mathlib.Algebra.Ring.Commute
  {R : Type u} [NonAssocRing R] [NoZeroDivisors R] {a : R} : a * a = 1 ↔ a = 1 ∨ a = -1
• mul_self_sub_one 📋 Mathlib.Algebra.Ring.Commute
  {R : Type u} [NonAssocRing R] (a : R) : a * a - 1 = (a + 1) * (a - 1)
• Int.castRingHom 📋 Mathlib.Data.Int.Cast.Lemmas
  (α : Type u_2) [NonAssocRing α] : ℤ →+* α
• RingHom.eq_intCast' 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] (f : ℤ →+* α) : f = Int.castRingHom α
• Commute.intCast_left 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] {a : α} {n : ℤ} : Commute (↑n) a
• Commute.intCast_right 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] {a : α} {n : ℤ} : Commute a ↑n
• Int.cast_commute 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] (n : ℤ) (a : α) : Commute (↑n) a
• Int.commute_cast 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] (a : α) (n : ℤ) : Commute a ↑n
• eq_intCast 📋 Mathlib.Data.Int.Cast.Lemmas
  {F : Type u_1} {α : Type u_2} [NonAssocRing α] [FunLike F ℤ α] [RingHomClass F ℤ α] (f : F) (n : ℤ) : f n = ↑n
• Int.coe_castRingHom 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] : ⇑(Int.castRingHom α) = fun x => ↑x
• map_intCast 📋 Mathlib.Data.Int.Cast.Lemmas
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [NonAssocRing α] [NonAssocRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (n : ℤ) : f ↑n = ↑n
• zsmul_eq_mul 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] (a : α) (n : ℤ) : n • a = ↑n * a
• zsmul_eq_mul' 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] (a : α) (n : ℤ) : n • a = a * ↑n
• Int.cast_comm 📋 Mathlib.Data.Int.Cast.Lemmas
  {α : Type u_2} [NonAssocRing α] (n : ℤ) (x : α) : ↑n * x = x * ↑n
• Int.smul_one_eq_cast 📋 Mathlib.Algebra.Module.NatInt
  {R : Type u_5} [NonAssocRing R] (m : ℤ) : m • 1 = ↑m
• Lex.instNonAssocRing 📋 Mathlib.Algebra.Order.Ring.Synonym
  {R : Type u_1} [NonAssocRing R] : NonAssocRing (Lex R)
• OrderDual.instNonAssocRing 📋 Mathlib.Algebra.Order.Ring.Synonym
  {R : Type u_1} [NonAssocRing R] : NonAssocRing Rᵒᵈ
• RingHom.injective_int 📋 Mathlib.Data.Int.CharZero
  {α : Type u_3} [NonAssocRing α] (f : ℤ →+* α) [CharZero α] : Function.Injective ⇑f
• MulRingNormClass 📋 Mathlib.Algebra.Order.Hom.Basic
  (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
• MulRingSeminormClass 📋 Mathlib.Algebra.Order.Hom.Basic
  (F : Type u_4) (α : outParam (Type u_5)) (β : outParam (Type u_6)) [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
• MulRingNormClass.toMulRingSeminormClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_4} {α : outParam (Type u_5)} {β : outParam (Type u_6)} {inst✝ : NonAssocRing α} {inst✝¹ : Semiring β} {inst✝² : PartialOrder β} {inst✝³ : FunLike F α β} [self : MulRingNormClass F α β] : MulRingSeminormClass F α β
• MulRingNormClass.toRingNormClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocRing α] [Semiring β] [PartialOrder β] [MulRingNormClass F α β] : RingNormClass F α β
• MulRingSeminormClass.toRingSeminormClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [NonAssocRing α] [Semiring β] [PartialOrder β] [MulRingSeminormClass F α β] : RingSeminormClass F α β
• MulRingSeminormClass.toMonoidWithZeroHomClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_4} {α : outParam (Type u_5)} {β : outParam (Type u_6)} [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] [self : MulRingSeminormClass F α β] : MonoidWithZeroHomClass F α β
• MulRingNormClass.toAddGroupNormClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_4} {α : outParam (Type u_5)} {β : outParam (Type u_6)} [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] [self : MulRingNormClass F α β] : AddGroupNormClass F α β
• MulRingSeminormClass.toAddGroupSeminormClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_4} {α : outParam (Type u_5)} {β : outParam (Type u_6)} {inst✝ : NonAssocRing α} {inst✝¹ : Semiring β} {inst✝² : PartialOrder β} {inst✝³ : FunLike F α β} [self : MulRingSeminormClass F α β] : AddGroupSeminormClass F α β
• MulRingSeminormClass.toMonoidHomClass 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_4} {α : outParam (Type u_5)} {β : outParam (Type u_6)} {inst✝ : NonAssocRing α} {inst✝¹ : Semiring β} {inst✝² : PartialOrder β} {inst✝³ : FunLike F α β} [self : MulRingSeminormClass F α β] : MonoidHomClass F α β
• MulRingSeminormClass.mk 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_4} {α : outParam (Type u_5)} {β : outParam (Type u_6)} [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] [toAddGroupSeminormClass : AddGroupSeminormClass F α β] [toMonoidHomClass : MonoidHomClass F α β] : MulRingSeminormClass F α β
• MulRingNormClass.eq_zero_of_map_eq_zero 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_4} {α : outParam (Type u_5)} {β : outParam (Type u_6)} {inst✝ : NonAssocRing α} {inst✝¹ : Semiring β} {inst✝² : PartialOrder β} {inst✝³ : FunLike F α β} [self : MulRingNormClass F α β] (f : F) {a : α} : f a = 0 → a = 0
• MulRingNormClass.mk 📋 Mathlib.Algebra.Order.Hom.Basic
  {F : Type u_4} {α : outParam (Type u_5)} {β : outParam (Type u_6)} [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] [toMulRingSeminormClass : MulRingSeminormClass F α β] (eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, f a = 0 → a = 0) : MulRingNormClass F α β
• RingEquiv.map_neg_one 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonAssocRing R] [NonAssocRing S] (f : R ≃+* S) : f (-1) = -1
• RingEquiv.map_eq_neg_one_iff 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonAssocRing R] [NonAssocRing S] (f : R ≃+* S) {x : R} : f x = -1 ↔ x = -1
• AddOpposite.instNonAssocRing 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_1} [NonAssocRing R] : NonAssocRing Rᵃᵒᵖ
• MulOpposite.instNonAssocRing 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_1} [NonAssocRing R] : NonAssocRing Rᵐᵒᵖ
• Pi.nonAssocRing 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} {f : I → Type v} [(i : I) → NonAssocRing (f i)] : NonAssocRing ((i : I) → f i)
• isSelfNeg_of_isSMulRegular_two 📋 Mathlib.Algebra.Module.Torsion.Free
  {R : Type u_1} [NonAssocRing R] (h : IsSMulRegular R 2) {a : R} : IsSelfNeg a ↔ a = 0
• ULift.nonAssocRing 📋 Mathlib.Algebra.Ring.ULift
  {R : Type u} [NonAssocRing R] : NonAssocRing (ULift.{u_1, u} R)
• CharZero.eq_neg_self_iff 📋 Mathlib.Algebra.Ring.CharZero
  {R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} : a = -a ↔ a = 0
• CharZero.neg_eq_self_iff 📋 Mathlib.Algebra.Ring.CharZero
  {R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R} : -a = a ↔ a = 0
• nat_mul_inj' 📋 Mathlib.Algebra.Ring.CharZero
  {R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a b : R} (h : ↑n * a = ↑n * b) (w : n ≠ 0) : a = b
• nat_mul_inj 📋 Mathlib.Algebra.Ring.CharZero
  {R : Type u_2} [NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a b : R} (h : ↑n * a = ↑n * b) : n = 0 ∨ a = b
• Subring 📋 Mathlib.Algebra.Ring.Subring.Defs
  (R : Type u) [NonAssocRing R] : Type u
• Subring.instPartialOrder 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : PartialOrder (Subring R)
• Subring.instSetLike 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : SetLike (Subring R) R
• SubringClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  (S : Type u_1) (R : outParam (Type u)) [NonAssocRing R] [SetLike S R] : Prop
• Subring.toNonUnitalSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) : NonUnitalSubring R
• Subring.toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (self : Subring R) : Subsemiring R
• Subring.instSubringClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : SubringClass (Subring R) R
• Subring.toAddSubgroup 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (self : Subring R) : AddSubgroup R
• Subring.toSubsemiring_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : Function.Injective Subring.toSubsemiring
• Subring.ofClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  {S : Type u_1} {R : Type u_2} [NonAssocRing R] [SetLike S R] [SubringClass S R] (s : S) : Subring R
• Subring.toAddSubgroup_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : Function.Injective Subring.toAddSubgroup
• SubringClass.nonUnitalSubringClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  (S : Type u_1) (R : Type u) [SetLike S R] [NonAssocRing R] [SubringClass S R] : NonUnitalSubringClass S R
• SubringClass.toSubsemiringClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  {S : Type u_1} {R : outParam (Type u)} {inst✝ : NonAssocRing R} {inst✝¹ : SetLike S R} [self : SubringClass S R] : SubsemiringClass S R
• Subring.toNonUnitalSubring_toSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) : S.toNonUnitalSubring.toSubring ⋯ = S
• Subring.copy 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S) : Subring R
• SubringClass.addSubgroupClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  (S : Type u_1) (R : Type u) [SetLike S R] [NonAssocRing R] [h : SubringClass S R] : AddSubgroupClass S R
• SubringClass.toHasIntCast 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] (s : S) : IntCast ↥s
• SubringClass.toNonAssocRing 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] (s : S) : NonAssocRing ↥s
• Subring.instNontrivialSubtypeMem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [NonAssocRing R] [Nontrivial R] (s : Subring R) : Nontrivial ↥s
• Subring.toSubmonoid_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : Function.Injective fun s => s.toSubmonoid
• Subring.toSubsemiring_inj 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s t : Subring R} : s.toSubsemiring = t.toSubsemiring ↔ s = t
• intCast_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℤ) : ↑n ∈ s
• Subring.copy_eq 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S
• SubringClass.toNegMemClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  {S : Type u_1} {R : outParam (Type u)} {inst✝ : NonAssocRing R} {inst✝¹ : SetLike S R} [self : SubringClass S R] : NegMemClass S R
• Subring.coe_toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑s.toSubsemiring = ↑s
• Subring.one_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : 1 ∈ s
• Subring.zero_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : 0 ∈ s
• Subring.coe_ofClass 📋 Mathlib.Algebra.Ring.Subring.Defs
  {S : Type u_1} {R : Type u_2} [NonAssocRing R] [SetLike S R] [SubringClass S R] (s : S) : ↑(Subring.ofClass s) = ↑s
• Subring.coe_copy 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S) : ↑(S.copy s hs) = s
• SubringClass.mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {S : Type u_1} {R : outParam (Type u)} [NonAssocRing R] [SetLike S R] [toSubsemiringClass : SubsemiringClass S R] [toNegMemClass : NegMemClass S R] : SubringClass S R
• Subring.coe_toAddSubgroup 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑s.toAddSubgroup = ↑s
• Subring.one_mem_toNonUnitalSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) : 1 ∈ S.toNonUnitalSubring
• NonUnitalSubring.toSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : NonUnitalSubring R) (h1 : 1 ∈ S) : Subring R
• Subring.coe_toSubmonoid 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑s.toSubmonoid = ↑s
• Subring.ext 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {S T : Subring R} (h : ∀ (x : R), x ∈ S ↔ x ∈ T) : S = T
• Subring.mem_toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} {x : R} : x ∈ s.toSubsemiring ↔ x ∈ s
• Subring.ext_iff 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {S T : Subring R} : S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T
• SubringClass.subtype 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] (s : S) : ↥s →+* R
• Subring.neg_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x : R} : x ∈ s → -x ∈ s
• NonUnitalSubring.toSubring_toNonUnitalSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : NonUnitalSubring R) (h1 : 1 ∈ S) : (S.toSubring h1).toNonUnitalSubring = S
• Subring.mem_toAddSubgroup 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} {x : R} : x ∈ s.toAddSubgroup ↔ x ∈ s
• Subring.zsmul_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s
• Subring.mem_carrier 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} {x : R} : x ∈ s.carrier ↔ x ∈ s
• Subring.subtype 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↥s →+* R
• Subsemiring.toSubring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subsemiring R) (hneg : -1 ∈ s) : Subring R
• Subring.mem_toSubmonoid 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} {x : R} : x ∈ s.toSubmonoid ↔ x ∈ s
• Subring.add_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x y : R} : x ∈ s → y ∈ s → x + y ∈ s
• Subring.mul_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x y : R} : x ∈ s → y ∈ s → x * y ∈ s
• Subring.sub_mem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s
• Subsemiring.toSubring_toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subsemiring R) (hneg : -1 ∈ s) : (s.toSubring hneg).toSubsemiring = s
• Subring.mk' 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : Subring R
• Subring.copy_toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S) : (S.copy s hs).toSubsemiring = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
• Subring.coe_mk' 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s) (ha : ↑sa = s) : ↑(Subring.mk' s sm sa hm ha) = s
• Subring.mk'_toAddSubgroup 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (Subring.mk' s sm sa hm ha).toAddSubgroup = sa
• SubringClass.coe_intCast 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℤ) : ↑↑n = ↑n
• Subring.mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (toSubsemiring : Subsemiring R) (neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier) : Subring R
• Subring.mk'_toSubmonoid 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) : (Subring.mk' s sm sa hm ha).toSubmonoid = sm
• Subring.neg_mem' 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (self : Subring R) {x : R} : x ∈ self.carrier → -x ∈ self.carrier
• Subring.mem_mk' 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) {x : R} : x ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s
• SubringClass.coe_natCast 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] (s : S) (n : ℕ) : ↑↑n = ↑n
• Subring.coe_set_mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (S : Subsemiring R) (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : ↑{ toSubsemiring := S, neg_mem' := h } = ↑S
• Subring.coe_intCast 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (n : ℤ) : ↑↑n = ↑n
• SubringClass.subtype_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] (s : S) : Function.Injective ⇑(SubringClass.subtype s)
• Subring.coe_one 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑1 = 1
• Subring.coe_neg 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (x : ↥s) : ↑(-x) = -↑x
• Subring.mem_mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {S : Subsemiring R} {x : R} (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) : x ∈ { toSubsemiring := S, neg_mem' := h } ↔ x ∈ S
• Subring.coe_zero 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ↑0 = 0
• SubringClass.coe_subtype 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] (s : S) : ⇑(SubringClass.subtype s) = Subtype.val
• Subring.coe_natCast 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (n : ℕ) : ↑↑n = ↑n
• SubringClass.subtype_apply 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} {S : Type v} [NonAssocRing R] [SetLike S R] [hSR : SubringClass S R] {s : S} (x : ↥s) : (SubringClass.subtype s) x = ↑x
• Subring.subtype_injective 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : Function.Injective ⇑s.subtype
• Subring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] : CanLift (Set R) (Subring R) SetLike.coe fun s => 0 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : R}, x ∈ s → -x ∈ s
• Subring.mk_eq_zero 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x : R} (hx : x ∈ s) : ⟨x, hx⟩ = 0 ↔ x = 0
• Subring.coe_eq_zero_iff 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) {x : ↥s} : ↑x = 0 ↔ x = 0
• Subring.coe_subtype 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) : ⇑s.subtype = Subtype.val
• Subring.subtype_apply 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {s : Subring R} (x : ↥s) : s.subtype x = ↑x
• Subring.instNoZeroDivisorsSubtypeMem 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u_1} [NonAssocRing R] [NoZeroDivisors R] (s : Subring R) : NoZeroDivisors ↥s
• Subring.mk_le_mk 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] {S S' : Subsemiring R} (h₁ : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) (h₂ : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier) : { toSubsemiring := S, neg_mem' := h₁ } ≤ { toSubsemiring := S', neg_mem' := h₂ } ↔ S ≤ S'
• Subring.coe_add 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (x y : ↥s) : ↑(x + y) = ↑x + ↑y
• Subring.coe_mul 📋 Mathlib.Algebra.Ring.Subring.Defs
  {R : Type u} [NonAssocRing R] (s : Subring R) (x y : ↥s) : ↑(x * y) = ↑x * ↑y
• Prod.instNonAssocRing 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} [NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S)
• Set.intCast_mem_center 📋 Mathlib.Algebra.Ring.Center
  (M : Type u_1) [NonAssocRing M] (n : ℤ) : ↑n ∈ Set.center M
• Subring.center 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u) [NonAssocRing R] : Subring R
• Subring.instBot 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Bot (Subring R)
• Subring.instCompleteLattice 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : CompleteLattice (Subring R)
• Subring.instInfSet 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : InfSet (Subring R)
• Subring.instInhabited 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Inhabited (Subring R)
• Subring.instMin 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Min (Subring R)
• Subring.instTop 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Top (Subring R)
• Subring.closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Set R) : Subring R
• RingHom.range 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : Subring S
• Subring.closure_univ 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Subring.closure Set.univ = ⊤
• Subring.center_toSubsemiring 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u) [NonAssocRing R] : (Subring.center R).toSubsemiring = Subsemiring.center R
• Subring.comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Subring S) : Subring R
• Subring.map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) (s : Subring R) : Subring S
• Subring.prod 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (s : Subring R) (t : Subring S) : Subring (R × S)
• Subring.closure_empty 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Subring.closure ∅ = ⊥
• Subring.map_id 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Subring R) : Subring.map (RingHom.id R) s = s
• Subring.closure_eq 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Subring R) : Subring.closure ↑s = s
• Subring.coe_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : ↑⊤ = Set.univ
• Subring.subset_closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} : s ⊆ ↑(Subring.closure s)
• Subring.mem_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (x : R) : x ∈ ⊤
• RingHom.eqLocus 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Type v} [Semiring S] (f g : R →+* S) : Subring R
• Subring.coe_center 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u) [NonAssocRing R] : ↑(Subring.center R) = Set.center R
• Subring.instFintypeSubtypeMemTop 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u_1} [NonAssocRing R] [Fintype R] : Fintype ↥⊤
• Subring.toSubsemiring_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : ⊤.toSubsemiring = ⊤
• Subring.mem_closure_of_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {x : R} (hx : x ∈ s) : x ∈ Subring.closure s
• RingHom.eqLocus_same 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {S : Type v} [Semiring S] (f : R →+* S) : f.eqLocus f = ⊤
• Subring.coe_bot 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : ↑⊥ = Set.range Int.cast
• Subring.toSubsemiring_mono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Monotone Subring.toSubsemiring
• Subring.toSubsemiring_strictMono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : StrictMono Subring.toSubsemiring
• Subring.closure_insert_intCast 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (n : ℤ) (s : Set R) : Subring.closure (insert (↑n) s) = Subring.closure s
• Subring.closure_singleton_intCast 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (n : ℤ) : Subring.closure {↑n} = ⊥
• Subring.notMem_of_notMem_closure 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {P : R} (hP : P ∉ Subring.closure s) : P ∉ s
• Subring.eq_top_iff' 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (A : Subring R) : A = ⊤ ↔ ∀ (x : R), x ∈ A
• Subring.center_prod 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] : Subring.center (R × S) = (Subring.center R).prod (Subring.center S)
• Subring.closure_insert_natCast 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (n : ℕ) (s : Set R) : Subring.closure (insert (↑n) s) = Subring.closure s
• Subring.closure_singleton_natCast 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (n : ℕ) : Subring.closure {↑n} = ⊥
• Subring.closure_insert_one 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Set R) : Subring.closure (insert 1 s) = Subring.closure s
• Subring.closure_insert_zero 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] (s : Set R) : Subring.closure (insert 0 s) = Subring.closure s
• Subring.closure_mono 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] ⦃s t : Set R⦄ (h : s ⊆ t) : Subring.closure s ≤ Subring.closure t
• Subring.closure_singleton_one 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Subring.closure {1} = ⊥
• Subring.closure_singleton_zero 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] : Subring.closure {0} = ⊥
• RingHom.range_eq_map 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : f.range = Subring.map f ⊤
• Subring.card_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  (R : Type u_1) [NonAssocRing R] [Fintype R] : Fintype.card ↥⊤ = Fintype.card R
• Subring.comap_top 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : Subring.comap f ⊤ = ⊤
• Subring.map_bot 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : Subring.map f ⊥ = ⊥

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 ce5dd8c