Loogle!

Result

Found 47 declarations mentioning AddMemClass.add_mem.

• AddMemClass.add_mem 📋 Mathlib.Algebra.Group.Subsemigroup.Defs
  {S : Type u_3} {M : outParam (Type u_4)} {inst✝ : Add M} {inst✝¹ : SetLike S M} [self : AddMemClass S M] {s : S} {a b : M} : a ∈ s → b ∈ s → a + b ∈ s
• AddMemClass.mk_add_mk 📋 Mathlib.Algebra.Group.Subsemigroup.Defs
  {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : M) (hx : x ∈ S') (hy : y ∈ S') : ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
• AddMemClass.add_def 📋 Mathlib.Algebra.Group.Subsemigroup.Defs
  {M : Type u_1} {A : Type u_3} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : ↥S') : x + y = ⟨↑x + ↑y, ⋯⟩
• AddSubsemigroup.closure_induction 📋 Mathlib.Algebra.Group.Subsemigroup.Basic
  {M : Type u_1} [Add M] {s : Set M} {p : (x : M) → x ∈ AddSubsemigroup.closure s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (add : ∀ (x y : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s), p x hx → p y hy → p (x + y) ⋯) {x : M} (hx : x ∈ AddSubsemigroup.closure s) : p x hx
• AddSubsemigroup.closure_induction₂ 📋 Mathlib.Algebra.Group.Subsemigroup.Basic
  {M : Type u_1} [Add M] {s : Set M} {p : (x y : M) → x ∈ AddSubsemigroup.closure s → y ∈ AddSubsemigroup.closure s → Prop} (mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (add_left : ∀ (x y z : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s) (hz : z ∈ AddSubsemigroup.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s) (hz : z ∈ AddSubsemigroup.closure s), p z x hz hx → p z y hz hy → p z (x + y) hz ⋯) {x y : M} (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s) : p x y hx hy
• 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
• AddSubsemigroup.iSup_induction' 📋 Mathlib.Algebra.Group.Subsemigroup.Membership
  {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι → AddSubsemigroup M) {C : (x : M) → x ∈ ⨆ i, S i → Prop} (mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) (add : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯) {x₁ : M} (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
• Submodule.mul_induction_on' 📋 Mathlib.Algebra.Algebra.Operations
  {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] [IsScalarTower R A A] {M N : Submodule R A} {C : (r : A) → r ∈ M * N → Prop} (mem_mul_mem : ∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N), C (m * n) ⋯) (add : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) ⋯) {r : A} (hr : r ∈ M * N) : C r hr
• Submodule.smul_induction_on' 📋 Mathlib.Algebra.Algebra.Operations
  {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] {I : Submodule R A} {N : Submodule R M} {x : M} (hx : x ∈ I • N) {p : (x : M) → x ∈ I • N → Prop} (smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯) (add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯) : p x hx
• Submodule.pow_induction_on_right' 📋 Mathlib.Algebra.Algebra.Operations
  {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop} (algebraMap : ∀ (r : R), C 0 ((algebraMap R A) r) ⋯) (add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) (mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯) {n : ℕ} {x : A} (hx : x ∈ M ^ n) : C n x hx
• Submodule.pow_induction_on_left' 📋 Mathlib.Algebra.Algebra.Operations
  {R : Type u} [CommSemiring R] {A : Type v} [Semiring A] [Algebra R A] (M : Submodule R A) {C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop} (algebraMap : ∀ (r : R), C 0 ((algebraMap R A) r) ⋯) (add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) (mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯) {n : ℕ} {x : A} (hx : x ∈ M ^ n) : C n 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
• Algebra.adjoin_induction 📋 Mathlib.Algebra.Algebra.Subalgebra.Lattice
  {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {p : (x : A) → x ∈ Algebra.adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (algebraMap : ∀ (r : R), p ((algebraMap R A) r) ⋯) (add : ∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (mul : ∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) {x : A} (hx : x ∈ Algebra.adjoin R s) : p x hx
• Algebra.iSup_induction' 📋 Mathlib.Algebra.Algebra.Subalgebra.Lattice
  {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} (S : ι → Subalgebra R A) {motive : (x : A) → x ∈ ⨆ i, S i → Prop} {x : A} (mem : x ∈ ⨆ i, S i) (basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯) (add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯) (mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯) (algebraMap : ∀ (r : R), motive ((algebraMap R A) r) ⋯) : motive x mem
• Algebra.adjoin_induction₂ 📋 Mathlib.Algebra.Algebra.Subalgebra.Lattice
  {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {p : (x y : A) → x ∈ Algebra.adjoin R s → y ∈ Algebra.adjoin R s → Prop} (mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯) (algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯) (algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯) (add_left : ∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.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 ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.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 ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.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 ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) {x y : A} (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) : p x y hx hy
• Subfield.closure_induction 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} [DivisionRing K] {s : Set K} {p : (x : K) → x ∈ Subfield.closure s → Prop} (mem : ∀ (x : K) (hx : x ∈ s), p x ⋯) (one : p 1 ⋯) (add : ∀ (x y : K) (hx : x ∈ Subfield.closure s) (hy : y ∈ Subfield.closure s), p x hx → p y hy → p (x + y) ⋯) (neg : ∀ (x : K) (hx : x ∈ Subfield.closure s), p x hx → p (-x) ⋯) (inv : ∀ (x : K) (hx : x ∈ Subfield.closure s), p x hx → p x⁻¹ ⋯) (mul : ∀ (x y : K) (hx : x ∈ Subfield.closure s) (hy : y ∈ Subfield.closure s), p x hx → p y hy → p (x * y) ⋯) {x : K} (h : x ∈ Subfield.closure s) : p x h
• 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
• StarAlgebra.adjoin_induction 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} {p : (x : A) → x ∈ StarAlgebra.adjoin R s → Prop} (mem : ∀ (x : A) (h : x ∈ s), p x ⋯) (algebraMap : ∀ (r : R), p ((algebraMap R A) r) ⋯) (add : ∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (mul : ∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) (star : ∀ (x : A) (hx : x ∈ StarAlgebra.adjoin R s), p x hx → p (star x) ⋯) {a : A} (ha : a ∈ StarAlgebra.adjoin R s) : p a ha
• StarAlgebra.adjoin_induction₂ 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] {s : Set A} {p : (x y : A) → x ∈ StarAlgebra.adjoin R s → y ∈ StarAlgebra.adjoin R s → Prop} (mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯) (algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯) (algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯) (add_left : ∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s) (hz : z ∈ StarAlgebra.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 ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s) (hz : z ∈ StarAlgebra.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 ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s) (hz : z ∈ StarAlgebra.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 ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s) (hz : z ∈ StarAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) (star_left : ∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s), p x y hx hy → p (star x) y ⋯ hy) (star_right : ∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s), p x y hx hy → p x (star y) hx ⋯) {a b : A} (ha : a ∈ StarAlgebra.adjoin R s) (hb : b ∈ StarAlgebra.adjoin R s) : p a b ha hb
• AddSubmonoid.saturation_induction 📋 Mathlib.Algebra.Group.Submonoid.Saturation
  {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} {p : (x : M) → x ∈ s.saturation → Prop} (mem : ∀ (x : M) (hx : x ∈ s), p x ⋯) (add : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x + y) ⋯) (of_add : ∀ (x y : M) (hxy : x + y ∈ s.saturation), p (x + y) hxy → p x ⋯ ∧ p y ⋯) {x : M} (hx : x ∈ s.saturation) : p x hx
• 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
• LieSubmodule.lieSpan_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] {s : Set M} {p : (x : M) → x ∈ LieSubmodule.lieSpan R L s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ LieSubmodule.lieSpan R L s) (hy : y ∈ LieSubmodule.lieSpan R L s), p x hx → p y hy → p (x + y) ⋯) (smul : ∀ (a : R) (x : M) (hx : x ∈ LieSubmodule.lieSpan R L s), p x hx → p (a • x) ⋯) {x : M} (lie : ∀ (x : L) (y : M) (hy : y ∈ LieSubmodule.lieSpan R L s), p y hy → p ⁅x, y⁆ ⋯) (hx : x ∈ LieSubmodule.lieSpan R L s) : p x hx
• IntermediateField.adjoin_induction 📋 Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
  (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {s : Set E} {p : (x : E) → x ∈ IntermediateField.adjoin F s → Prop} (mem : ∀ (x : E) (hx : x ∈ s), p x ⋯) (algebraMap : ∀ (x : F), p ((algebraMap F E) x) ⋯) (add : ∀ (x y : E) (hx : x ∈ IntermediateField.adjoin F s) (hy : y ∈ IntermediateField.adjoin F s), p x hx → p y hy → p (x + y) ⋯) (inv : ∀ (x : E) (hx : x ∈ IntermediateField.adjoin F s), p x hx → p x⁻¹ ⋯) (mul : ∀ (x y : E) (hx : x ∈ IntermediateField.adjoin F s) (hy : y ∈ IntermediateField.adjoin F s), p x hx → p y hy → p (x * y) ⋯) {x : E} (h : x ∈ IntermediateField.adjoin F s) : p x h
• NumberField.RingOfIntegers.mk_add_mk 📋 Mathlib.NumberTheory.NumberField.Basic
  {K : Type u_1} [Field K] (x y : K) (hx : x ∈ integralClosure ℤ K) (hy : y ∈ integralClosure ℤ K) : ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
• StarAlgebra.elemental.induction_on 📋 Mathlib.Topology.Algebra.StarSubalgebra
  (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [StarRing A] [IsSemitopologicalSemiring A] [ContinuousStar A] [Algebra R A] [StarModule R A] {x y : A} (hy : y ∈ StarAlgebra.elemental R x) {P : (u : A) → u ∈ StarAlgebra.elemental R x → Prop} (self : P x ⋯) (star_self : P (star x) ⋯) (algebraMap : ∀ (r : R), P ((algebraMap R A) r) ⋯) (add : ∀ (u : A) (hu : u ∈ StarAlgebra.elemental R x) (v : A) (hv : v ∈ StarAlgebra.elemental R x), P u hu → P v hv → P (u + v) ⋯) (mul : ∀ (u : A) (hu : u ∈ StarAlgebra.elemental R x) (v : A) (hv : v ∈ StarAlgebra.elemental R x), P u hu → P v hv → P (u * v) ⋯) (closure : ∀ (s : Set A) (hs : s ⊆ ↑(StarAlgebra.elemental R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure s), P v ⋯) : P y hy
• solvableByRad.induction 📋 Mathlib.FieldTheory.AbelRuffini
  {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (motive : (x : E) → x ∈ solvableByRad F E → Prop) (mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯) (add : ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯) (mul : ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯) (rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯) {x : E} (hx : x ∈ solvableByRad F E) : motive x hx

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