Loogle!

Result

Found 28 declarations mentioning ZeroMemClass.zero_mem.

• ZeroMemClass.zero_mem 📋 Mathlib.Algebra.Group.Submonoid.Defs
  {S : Type u_3} {M : outParam (Type u_4)} {inst✝ : Zero M} {inst✝¹ : SetLike S M} [self : ZeroMemClass S M] (s : S) : 0 ∈ s
• ZeroMemClass.zero_def 📋 Mathlib.Algebra.Group.Submonoid.Defs
  {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : 0 = ⟨0, ⋯⟩
• AddSubmonoid.closure_induction 📋 Mathlib.Algebra.Group.Submonoid.Basic
  {M : Type u_1} [AddZeroClass M] {s : Set M} {motive : (x : M) → x ∈ AddSubmonoid.closure s → Prop} (mem : ∀ (x : M) (h : x ∈ s), motive x ⋯) (zero : motive 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s), motive x hx → motive y hy → motive (x + y) ⋯) {x : M} (hx : x ∈ AddSubmonoid.closure s) : motive x hx
• AddSubmonoid.closure_induction₂ 📋 Mathlib.Algebra.Group.Submonoid.Basic
  {M : Type u_1} [AddZeroClass M] {s : Set M} {motive : (x y : M) → x ∈ AddSubmonoid.closure s → y ∈ AddSubmonoid.closure s → Prop} (mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯) (zero_left : ∀ (x : M) (hx : x ∈ AddSubmonoid.closure s), motive 0 x ⋯ hx) (zero_right : ∀ (x : M) (hx : x ∈ AddSubmonoid.closure s), motive x 0 hx ⋯) (add_left : ∀ (x y z : M) (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s) (hz : z ∈ AddSubmonoid.closure s), motive x z hx hz → motive y z hy hz → motive (x + y) z ⋯ hz) (add_right : ∀ (x y z : M) (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s) (hz : z ∈ AddSubmonoid.closure s), motive z x hz hx → motive z y hz hy → motive z (x + y) hz ⋯) {x y : M} (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s) : motive x y hx hy
• AddSubgroup.closure_induction 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [AddGroup G] {k : Set G} {p : (g : G) → g ∈ AddSubgroup.closure k → Prop} (mem : ∀ (x : G) (hx : x ∈ k), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x hx → p y hy → p (x + y) ⋯) (neg : ∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x hx → p (-x) ⋯) {x : G} (hx : x ∈ AddSubgroup.closure k) : p x hx
• AddSubgroup.closure_induction₂ 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [AddGroup G] {k : Set G} {p : (x y : G) → x ∈ AddSubgroup.closure k → y ∈ AddSubgroup.closure k → Prop} (mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯) (zero_left : ∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p 0 x ⋯ hx) (zero_right : ∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x 0 hx ⋯) (add_left : ∀ (x y z : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k) (hz : z ∈ AddSubgroup.closure k), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (y z x : G) (hy : y ∈ AddSubgroup.closure k) (hz : z ∈ AddSubgroup.closure k) (hx : x ∈ AddSubgroup.closure k), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (neg_left : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x y hx hy → p (-x) y ⋯ hy) (neg_right : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x y hx hy → p x (-y) hx ⋯) {x y : G} (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k) : p x y hx hy
• AddSubmonoid.closure_induction_left 📋 Mathlib.Algebra.Group.Submonoid.Membership
  {M : Type u_1} [AddMonoid M] {s : Set M} {motive : (m : M) → m ∈ AddSubmonoid.closure s → Prop} (zero : motive 0 ⋯) (add_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ AddSubmonoid.closure s), motive y hy → motive (x + y) ⋯) {x : M} (h : x ∈ AddSubmonoid.closure s) : motive x h
• AddSubmonoid.closure_induction_right 📋 Mathlib.Algebra.Group.Submonoid.Membership
  {M : Type u_1} [AddMonoid M] {s : Set M} {motive : (m : M) → m ∈ AddSubmonoid.closure s → Prop} (zero : motive 0 ⋯) (add_right : ∀ (x : M) (hx : x ∈ AddSubmonoid.closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x + y) ⋯) {x : M} (h : x ∈ AddSubmonoid.closure s) : motive x h
• AddSubmonoid.iSup_induction' 📋 Mathlib.Algebra.Group.Submonoid.Membership
  {M : Type u_1} [AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid M) {motive : (x : M) → x ∈ ⨆ i, S i → Prop} (mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯) (zero : motive 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯) {x : M} (hx : x ∈ ⨆ i, S i) : motive x hx
• AddSubgroup.closure_induction'' 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] {s : Set G} {p : (g : G) → g ∈ AddSubgroup.closure s → Prop} (mem : ∀ (x : G) (hx : x ∈ s), p x ⋯) (neg_mem : ∀ (x : G) (hx : x ∈ s), p (-x) ⋯) (zero : p 0 ⋯) (add : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure s) (hy : y ∈ AddSubgroup.closure s), p x hx → p y hy → p (x + y) ⋯) {x : G} (h : x ∈ AddSubgroup.closure s) : p x h
• AddSubgroup.closure_induction_left 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] {s : Set G} {p : (x : G) → x ∈ AddSubgroup.closure s → Prop} (zero : p 0 ⋯) (add_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (x + y) ⋯) (neg_add_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (-x + y) ⋯) {x : G} (h : x ∈ AddSubgroup.closure s) : p x h
• AddSubgroup.closure_induction_right 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] {s : Set G} {p : (x : G) → x ∈ AddSubgroup.closure s → Prop} (zero : p 0 ⋯) (add_right : ∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + y) ⋯) (add_neg_cancel : ∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + -y) ⋯) {x : G} (h : x ∈ AddSubgroup.closure s) : p x h
• AddSubgroup.iSup_induction' 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] {ι : Sort u_5} (S : ι → AddSubgroup G) {C : (x : G) → x ∈ ⨆ i, S i → Prop} (hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯) (h1 : C 0 ⋯) (hadd : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯) {x : G} (hx : x ∈ ⨆ i, S i) : C x hx
• NonUnitalSubsemiring.closure_induction 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {p : (x : R) → x ∈ NonUnitalSubsemiring.closure s → Prop} (mem : ∀ (x : R) (hx : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s), p x hx → p y hy → p (x + y) ⋯) (mul : ∀ (x y : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s), p x hx → p y hy → p (x * y) ⋯) {x : R} (hx : x ∈ NonUnitalSubsemiring.closure s) : p x hx
• NonUnitalSubsemiring.closure_induction₂ 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {p : (x y : R) → x ∈ NonUnitalSubsemiring.closure s → y ∈ NonUnitalSubsemiring.closure s → Prop} (mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (x : R) (hx : x ∈ NonUnitalSubsemiring.closure s), p 0 x ⋯ hx) (zero_right : ∀ (x : R) (hx : x ∈ NonUnitalSubsemiring.closure s), p x 0 hx ⋯) (add_left : ∀ (x y z : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s) (hz : z ∈ NonUnitalSubsemiring.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s) (hz : z ∈ NonUnitalSubsemiring.closure s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (mul_left : ∀ (x y z : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s) (hz : z ∈ NonUnitalSubsemiring.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : R) (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s) (hz : z ∈ NonUnitalSubsemiring.closure s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) {x y : R} (hx : x ∈ NonUnitalSubsemiring.closure s) (hy : y ∈ NonUnitalSubsemiring.closure s) : p x y hx hy
• Subsemiring.closure_induction 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} [NonAssocSemiring R] {s : Set R} {p : (x : R) → x ∈ Subsemiring.closure s → Prop} (mem : ∀ (x : R) (hx : x ∈ s), p x ⋯) (zero : p 0 ⋯) (one : p 1 ⋯) (add : ∀ (x y : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s), p x hx → p y hy → p (x + y) ⋯) (mul : ∀ (x y : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s), p x hx → p y hy → p (x * y) ⋯) {x : R} (hx : x ∈ Subsemiring.closure s) : p x hx
• Subsemiring.closure_induction₂ 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} [NonAssocSemiring R] {s : Set R} {p : (x y : R) → x ∈ Subsemiring.closure s → y ∈ Subsemiring.closure s → Prop} (mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (x : R) (hx : x ∈ Subsemiring.closure s), p 0 x ⋯ hx) (zero_right : ∀ (x : R) (hx : x ∈ Subsemiring.closure s), p x 0 hx ⋯) (one_left : ∀ (x : R) (hx : x ∈ Subsemiring.closure s), p 1 x ⋯ hx) (one_right : ∀ (x : R) (hx : x ∈ Subsemiring.closure s), p x 1 hx ⋯) (add_left : ∀ (x y z : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s) (hz : z ∈ Subsemiring.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s) (hz : z ∈ Subsemiring.closure s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (mul_left : ∀ (x y z : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s) (hz : z ∈ Subsemiring.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s) (hz : z ∈ Subsemiring.closure s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) {x y : R} (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s) : p x y hx hy
• NonUnitalSubring.closure_induction 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {p : (x : R) → x ∈ NonUnitalSubring.closure s → Prop} (mem : ∀ (x : R) (hx : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s), p x hx → p y hy → p (x + y) ⋯) (neg : ∀ (x : R) (hx : x ∈ NonUnitalSubring.closure s), p x hx → p (-x) ⋯) (mul : ∀ (x y : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s), p x hx → p y hy → p (x * y) ⋯) {x : R} (hx : x ∈ NonUnitalSubring.closure s) : p x hx
• NonUnitalSubring.closure_induction₂ 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} [NonUnitalNonAssocRing R] {s : Set R} {p : (x y : R) → x ∈ NonUnitalSubring.closure s → y ∈ NonUnitalSubring.closure s → Prop} (mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (x : R) (hx : x ∈ NonUnitalSubring.closure s), p 0 x ⋯ hx) (zero_right : ∀ (x : R) (hx : x ∈ NonUnitalSubring.closure s), p x 0 hx ⋯) (neg_left : ∀ (x y : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s), p x y hx hy → p (-x) y ⋯ hy) (neg_right : ∀ (x y : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s), p x y hx hy → p x (-y) hx ⋯) (add_left : ∀ (x y z : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s) (hz : z ∈ NonUnitalSubring.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s) (hz : z ∈ NonUnitalSubring.closure s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (mul_left : ∀ (x y z : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s) (hz : z ∈ NonUnitalSubring.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s) (hz : z ∈ NonUnitalSubring.closure s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) {x y : R} (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s) : p x y hx hy
• Subring.closure_induction 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {p : (x : R) → x ∈ Subring.closure s → Prop} (mem : ∀ (x : R) (hx : x ∈ s), p x ⋯) (zero : p 0 ⋯) (one : p 1 ⋯) (add : ∀ (x y : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x hx → p y hy → p (x + y) ⋯) (neg : ∀ (x : R) (hx : x ∈ Subring.closure s), p x hx → p (-x) ⋯) (mul : ∀ (x y : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x hx → p y hy → p (x * y) ⋯) {x : R} (hx : x ∈ Subring.closure s) : p x hx
• Subring.closure_induction₂ 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [NonAssocRing R] {s : Set R} {p : (x y : R) → x ∈ Subring.closure s → y ∈ Subring.closure s → Prop} (mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (x : R) (hx : x ∈ Subring.closure s), p 0 x ⋯ hx) (zero_right : ∀ (x : R) (hx : x ∈ Subring.closure s), p x 0 hx ⋯) (one_left : ∀ (x : R) (hx : x ∈ Subring.closure s), p 1 x ⋯ hx) (one_right : ∀ (x : R) (hx : x ∈ Subring.closure s), p x 1 hx ⋯) (neg_left : ∀ (x y : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x y hx hy → p (-x) y ⋯ hy) (neg_right : ∀ (x y : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x y hx hy → p x (-y) hx ⋯) (add_left : ∀ (x y z : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s) (hz : z ∈ Subring.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s) (hz : z ∈ Subring.closure s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (mul_left : ∀ (x y z : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s) (hz : z ∈ Subring.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s) (hz : z ∈ Subring.closure s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) {x y : R} (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s) : p x y hx hy
• Submodule.span_induction₂ 📋 Mathlib.LinearAlgebra.Span.Defs
  {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {N : Type u_6} [AddCommMonoid N] [Module R N] {t : Set N} {p : (x : M) → (y : N) → x ∈ Submodule.span R s → y ∈ Submodule.span R t → Prop} (mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯) (zero_left : ∀ (y : N) (hy : y ∈ Submodule.span R t), p 0 y ⋯ hy) (zero_right : ∀ (x : M) (hx : x ∈ Submodule.span R s), p x 0 hx ⋯) (add_left : ∀ (x y : M) (z : N) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s) (hz : z ∈ Submodule.span R t), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x : M) (y z : N) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R t) (hz : z ∈ Submodule.span R t), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R t), p x y hx hy → p (r • x) y ⋯ hy) (smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R t), p x y hx hy → p x (r • y) hx ⋯) {a : M} {b : N} (ha : a ∈ Submodule.span R s) (hb : b ∈ Submodule.span R t) : p a b ha hb
• Submodule.iSup_induction' 📋 Mathlib.LinearAlgebra.Span.Basic
  {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_8} (p : ι → Submodule R M) {motive : (x : M) → x ∈ ⨆ i, p i → Prop} (mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯) (zero : motive 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯) {x : M} (hx : x ∈ ⨆ i, p i) : motive x hx
• NonUnitalAlgebra.adjoin_induction 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : (x : A) → x ∈ NonUnitalAlgebra.adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (add : ∀ (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (zero : p 0 ⋯) (mul : ∀ (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) (smul : ∀ (r : R) (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x hx → p (r • x) ⋯) {x : A} (hx : x ∈ NonUnitalAlgebra.adjoin R s) : p x hx
• NonUnitalAlgebra.adjoin_induction₂ 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : (x y : A) → x ∈ NonUnitalAlgebra.adjoin R s → y ∈ NonUnitalAlgebra.adjoin R s → Prop} (mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p 0 x ⋯ hx) (zero_right : ∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x 0 hx ⋯) (add_left : ∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (mul_left : ∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) (hz : z ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) (smul_left : ∀ (r : R) (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p (r • x) y ⋯ hy) (smul_right : ∀ (r : R) (x y : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x y hx hy → p x (r • y) hx ⋯) {x y : A} (hx : x ∈ NonUnitalAlgebra.adjoin R s) (hy : y ∈ NonUnitalAlgebra.adjoin R s) : p x y hx hy
• NonUnitalStarAlgebra.adjoin_induction 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  (R : Type u) {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] {s : Set A} {p : (x : A) → x ∈ NonUnitalStarAlgebra.adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (add : ∀ (x y : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (zero : p 0 ⋯) (mul : ∀ (x y : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) (smul : ∀ (r : R) (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (r • x) ⋯) (star : ∀ (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (star x) ⋯) {a : A} (ha : a ∈ NonUnitalStarAlgebra.adjoin R s) : p a ha
• LieSubmodule.iSup_induction' 📋 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] {ι : Sort u_1} (N : ι → LieSubmodule R L M) {motive : (x : M) → x ∈ ⨆ i, N i → Prop} (mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯) (zero : motive 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯) {x : M} (hx : x ∈ ⨆ i, N i) : motive x hx
• NumberField.RingOfIntegers.mk_zero 📋 Mathlib.NumberTheory.NumberField.Basic
  {K : Type u_1} [Field K] : ⟨0, ⋯⟩ = 0

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