Loogle!

Result

Found 203 declarations mentioning NonUnitalRingHom. Of these, only the first 200 are shown.

• NonUnitalRingHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  (α : Type u_5) (β : Type u_6) [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Type (max u_5 u_6)
• NonUnitalRingHom.id 📋 Mathlib.Algebra.Ring.Hom.Defs
  (α : Type u_5) [NonUnitalNonAssocSemiring α] : α →ₙ+* α
• NonUnitalRingHom.instMonoidWithZero 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} [NonUnitalNonAssocSemiring α] : MonoidWithZero (α →ₙ+* α)
• NonUnitalRingHom.instInhabited 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Inhabited (α →ₙ+* β)
• NonUnitalRingHom.instZero 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Zero (α →ₙ+* β)
• NonUnitalRingHom.instFunLike 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : FunLike (α →ₙ+* β) α β
• RingHom.toNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_5} {β : Type u_6} [NonAssocSemiring α] [NonAssocSemiring β] (self : α →+* β) : α →ₙ+* β
• NonUnitalRingHom.instNonUnitalRingHomClass 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : NonUnitalRingHomClass (α →ₙ+* β) α β
• NonUnitalRingHom.comp 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) : α →ₙ+* γ
• NonUnitalRingHom.toMulHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_5} {β : Type u_6} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (self : α →ₙ+* β) : α →ₙ* β
• NonUnitalRingHomClass.toNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [FunLike F α β] [NonUnitalRingHomClass F α β] (f : F) : α →ₙ+* β
• instCoeTCNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {F : Type u_1} {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [FunLike F α β] [NonUnitalRingHomClass F α β] : CoeTC F (α →ₙ+* β)
• NonUnitalRingHom.id_apply 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} [NonUnitalNonAssocSemiring α] (x : α) : (NonUnitalRingHom.id α) x = x
• NonUnitalRingHom.comp_id 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : f.comp (NonUnitalRingHom.id α) = f
• NonUnitalRingHom.id_comp 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : (NonUnitalRingHom.id β).comp f = f
• NonUnitalRingHom.toAddMonoidHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_5} {β : Type u_6} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (self : α →ₙ+* β) : α →+ β
• NonUnitalRingHom.copy 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f) : α →ₙ+* β
• NonUnitalRingHom.copy_eq 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f
• NonUnitalRingHom.one_def 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} [NonUnitalNonAssocSemiring α] : 1 = NonUnitalRingHom.id α
• NonUnitalRingHom.zero_apply 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (x : α) : 0 x = 0
• NonUnitalRingHom.coe_copy 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'
• NonUnitalRingHom.coe_zero 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : ⇑0 = 0
• NonUnitalRingHom.ext 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] ⦃f g : α →ₙ+* β⦄ : (∀ (x : α), f x = g x) → f = g
• NonUnitalRingHom.ext_iff 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] {f g : α →ₙ+* β} : f = g ↔ ∀ (x : α), f x = g x
• NonUnitalRingHom.coe_one 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} [NonUnitalNonAssocSemiring α] : ⇑1 = id
• NonUnitalRingHom.comp_zero 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) : g.comp 0 = 0
• NonUnitalRingHom.map_zero' 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_5} {β : Type u_6} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (self : α →ₙ+* β) : self.toFun 0 = 0
• NonUnitalRingHom.zero_comp 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (f : α →ₙ+* β) : NonUnitalRingHom.comp 0 f = 0
• NonUnitalRingHom.coe_toMulHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : ⇑f.toMulHom = ⇑f
• NonUnitalRingHom.comp_assoc 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {δ : Type u_5} {x✝ : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ) : (h.comp g).comp f = h.comp (g.comp f)
• NonUnitalRingHom.coe_mulHom_id 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} [NonUnitalNonAssocSemiring α] : ↑(NonUnitalRingHom.id α) = MulHom.id α
• NonUnitalRingHom.mul_def 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} [NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α) : f * g = f.comp g
• NonUnitalRingHom.coe_mulHom_injective 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Function.Injective fun f => ↑f
• NonUnitalRingHom.cancel_left 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
• NonUnitalRingHom.cancel_right 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂
• NonUnitalRingHom.comp_apply 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) : (g.comp f) x = g (f x)
• NonUnitalRingHom.coe_comp 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) : ⇑(g.comp f) = ⇑g ∘ ⇑f
• NonUnitalRingHom.coe_toAddMonoidHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : ⇑f.toAddMonoidHom = ⇑f
• NonUnitalRingHom.coe_addMonoidHom_id 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} [NonUnitalNonAssocSemiring α] : ↑(NonUnitalRingHom.id α) = AddMonoidHom.id α
• NonUnitalRingHom.coe_addMonoidHom_injective 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Function.Injective fun f => ↑f
• NonUnitalRingHom.coe_mul 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} [NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α) : ⇑(f * g) = ⇑f ∘ ⇑g
• NonUnitalRingHom.map_add' 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_5} {β : Type u_6} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (self : α →ₙ+* β) (x y : α) : self.toFun (x + y) = self.toFun x + self.toFun y
• NonUnitalRingHom.mk 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_5} {β : Type u_6} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (toMulHom : α →ₙ* β) (map_zero' : toMulHom.toFun 0 = 0) (map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y) : α →ₙ+* β
• NonUnitalRingHom.coe_comp_mulHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) : { toFun := ⇑g ∘ ⇑f, map_mul' := ⋯ } = (↑g).comp ↑f
• NonUnitalRingHom.coe_comp_addMonoidHom 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) : { toFun := ⇑g ∘ ⇑f, map_zero' := ⋯, map_add' := ⋯ } = (↑g).comp ↑f
• NonUnitalRingHom.coe_mulHom_mk 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α → β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y) : ↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_mul' := h₁ }
• NonUnitalRingHom.coe_addMonoidHom_mk 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α → β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y) : ↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_zero' := h₂, map_add' := h₃ }
• NonUnitalRingHom.mk_coe 📋 Mathlib.Algebra.Ring.Hom.Defs
  {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y) : { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = f
• RingEquiv.toNonUnitalRingHom_refl 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} [NonUnitalNonAssocSemiring R] : (RingEquiv.refl R).toNonUnitalRingHom = NonUnitalRingHom.id R
• RingEquiv.toNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) : R →ₙ+* S
• RingEquiv.toNonUnitalRingHom_injective 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : Function.Injective RingEquiv.toNonUnitalRingHom
• NonUnitalRingHom.inverse 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (g : S → R) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : S →ₙ+* R
• RingEquiv.ofNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (hom : R →ₙ+* S) (inv : S →ₙ+* R) (hom_inv_id : inv.comp hom = NonUnitalRingHom.id R) (inv_hom_id : hom.comp inv = NonUnitalRingHom.id S) : R ≃+* S
• NonUnitalRingHom.inverse_apply 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (g : S → R) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a✝ : S) : (f.inverse g h₁ h₂) a✝ = g a✝
• RingEquiv.symm_toNonUnitalRingHom_comp_toNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) : e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R
• RingEquiv.toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) : e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S
• RingEquiv.symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (x : R) : e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x
• RingEquiv.toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (y : S) : e.toNonUnitalRingHom (e.symm.toNonUnitalRingHom y) = y
• RingEquiv.symm_ofNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (g : S →ₙ+* R) (h₁ : g.comp f = NonUnitalRingHom.id R) (h₂ : f.comp g = NonUnitalRingHom.id S) : (RingEquiv.ofNonUnitalRingHom f g h₁ h₂).symm = RingEquiv.ofNonUnitalRingHom g f h₂ h₁
• RingEquiv.toNonUnitalRingHom_trans 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} {S' : Type u_6} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') : (e₁.trans e₂).toNonUnitalRingHom = e₂.toNonUnitalRingHom.comp e₁.toNonUnitalRingHom
• RingEquiv.coe_toNonUnitalRingHom' 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) : ⇑f.toNonUnitalRingHom = ⇑f
• RingEquiv.ofNonUnitalRingHom_apply 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (hom : R →ₙ+* S) (inv : S →ₙ+* R) (hom_inv_id : inv.comp hom = NonUnitalRingHom.id R) (inv_hom_id : hom.comp inv = NonUnitalRingHom.id S) (a : R) : (RingEquiv.ofNonUnitalRingHom hom inv hom_inv_id inv_hom_id) a = hom a
• RingEquiv.ofNonUnitalRingHom_symm_apply 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (hom : R →ₙ+* S) (inv : S →ₙ+* R) (hom_inv_id : inv.comp hom = NonUnitalRingHom.id R) (inv_hom_id : hom.comp inv = NonUnitalRingHom.id S) (a : S) : (RingEquiv.ofNonUnitalRingHom hom inv hom_inv_id inv_hom_id).symm a = inv a
• RingEquiv.toNonUnitalRingHom_eq_coe 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) : f.toNonUnitalRingHom = ↑f
• RingEquiv.comp_ofBijective_symm 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : Function.Bijective ⇑f) : f.comp ↑(RingEquiv.ofBijective f hf).symm = NonUnitalRingHom.id S
• RingEquiv.ofBijective_symm_comp 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : Function.Bijective ⇑f) : (↑(RingEquiv.ofBijective f hf).symm).comp f = NonUnitalRingHom.id R
• RingEquiv.coe_toNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) : ⇑↑f = ⇑f
• RingEquiv.coe_nonUnitalRingHom_inj_iff 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_7} {S : Type u_8} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f g : R ≃+* S) : f = g ↔ ↑f = ↑g
• RingEquiv.toNonUnitalRingHom_commutes 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) : ↑↑f = ↑f
• NonUnitalRingHom.op 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : (R →ₙ+* S) ≃ (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ)
• NonUnitalRingHom.unop 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) ≃ (R →ₙ+* S)
• NonUnitalRingHom.fromOpposite 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : Rᵐᵒᵖ →ₙ+* S
• NonUnitalRingHom.toOpposite 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : R →ₙ+* Sᵐᵒᵖ
• NonUnitalRingHom.toOpposite_apply 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
• NonUnitalRingHom.fromOpposite_apply 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
• NonUnitalRingHom.op_apply_apply 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (a✝ : Rᵐᵒᵖ) : (NonUnitalRingHom.op f) a✝ = (↑(AddMonoidHom.mulOp f.toAddMonoidHom)).toFun a✝
• NonUnitalRingHom.op_symm_apply_apply 📋 Mathlib.Algebra.Ring.Opposite
  {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) (a✝ : R) : (NonUnitalRingHom.op.symm f) a✝ = (↑(AddMonoidHom.mulUnop f.toAddMonoidHom)).toFun a✝
• Pi.constNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Pi
  (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] : β →ₙ+* α → β
• Pi.evalNonUnitalRingHom 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} (f : I → Type v) [(i : I) → NonUnitalNonAssocSemiring (f i)] (i : I) : ((i : I) → f i) →ₙ+* f i
• NonUnitalRingHom.pi 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) : γ →ₙ+* (i : I) → f i
• Pi.nonUnitalRingHom 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) : γ →ₙ+* (i : I) → f i
• NonUnitalRingHom.compLeft 📋 Mathlib.Algebra.Ring.Pi
  {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type u_3) : (I → α) →ₙ+* I → β
• Pi.constNonUnitalRingHom_apply 📋 Mathlib.Algebra.Ring.Pi
  (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] (a : β) (a✝ : α) : (Pi.constNonUnitalRingHom α β) a a✝ = Function.const α a a✝
• Pi.evalNonUnitalRingHom_apply 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} (f : I → Type v) [(i : I) → NonUnitalNonAssocSemiring (f i)] (i : I) (g : (i : I) → f i) : (Pi.evalNonUnitalRingHom f i) g = g i
• NonUnitalRingHom.pi_apply 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (x : γ) (b : I) : (NonUnitalRingHom.pi g) x b = (g b) x
• Pi.nonUnitalRingHom_apply 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (x : γ) (b : I) : (NonUnitalRingHom.pi g) x b = (g b) x
• NonUnitalRingHom.pi_injective 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(NonUnitalRingHom.pi g)
• Pi.nonUnitalRingHom_injective 📋 Mathlib.Algebra.Ring.Pi
  {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) : Function.Injective ⇑(NonUnitalRingHom.pi g)
• NonUnitalRingHom.compLeft_apply 📋 Mathlib.Algebra.Ring.Pi
  {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type u_3) (h : I → α) (a✝ : I) : (f.compLeft I) h a✝ = (⇑f ∘ h) a✝
• NonUnitalSubsemiringClass.subtype 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) : ↥s →ₙ+* R
• NonUnitalRingHom.codRestrict 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] {S' : Type u_2} [SetLike S' S] [NonUnitalSubsemiringClass S' S] (f : F) (s : S') (h : ∀ (x : R), f x ∈ s) : R →ₙ+* ↥s
• NonUnitalSubsemiring.inclusion 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} [NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R} (h : S ≤ T) : ↥S →ₙ+* ↥T
• NonUnitalSubsemiringClass.subtype_injective 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) : Function.Injective ⇑(NonUnitalSubsemiringClass.subtype s)
• NonUnitalSubsemiringClass.coe_subtype 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) : ⇑(NonUnitalSubsemiringClass.subtype s) = Subtype.val
• NonUnitalSubsemiringClass.subtype_apply 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] {s : S} (x : ↥s) : (NonUnitalSubsemiringClass.subtype s) x = ↑x
• NonUnitalSubringClass.subtype 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) : ↥s →ₙ+* R
• NonUnitalSubring.inclusion 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} [NonUnitalNonAssocRing R] {S T : NonUnitalSubring R} (h : S ≤ T) : ↥S →ₙ+* ↥T
• NonUnitalSubringClass.subtype_injective 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) : Function.Injective ⇑(NonUnitalSubringClass.subtype s)
• NonUnitalSubringClass.coe_subtype 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S) : ⇑(NonUnitalSubringClass.subtype s) = Subtype.val
• NonUnitalSubringClass.subtype_apply 📋 Mathlib.RingTheory.NonUnitalSubring.Defs
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [SetLike S R] [hSR : NonUnitalSubringClass S R] {s : S} (x : ↥s) : (NonUnitalSubringClass.subtype s) x = ↑x
• NonUnitalRingHom.fst 📋 Mathlib.Algebra.Ring.Prod
  (R : Type u_1) (S : Type u_3) [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : R × S →ₙ+* R
• NonUnitalRingHom.snd 📋 Mathlib.Algebra.Ring.Prod
  (R : Type u_1) (S : Type u_3) [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : R × S →ₙ+* S
• NonUnitalRingHom.prod 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) : R →ₙ+* S × T
• NonUnitalRingHom.prodMap 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') : R × S →ₙ+* R' × S'
• NonUnitalRingHom.coe_fst 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : ⇑(NonUnitalRingHom.fst R S) = Prod.fst
• NonUnitalRingHom.coe_snd 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : ⇑(NonUnitalRingHom.snd R S) = Prod.snd
• NonUnitalRingHom.fst_comp_prod 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) : (NonUnitalRingHom.fst S T).comp (f.prod g) = f
• NonUnitalRingHom.snd_comp_prod 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) : (NonUnitalRingHom.snd S T).comp (f.prod g) = g
• NonUnitalRingHom.prod_unique 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S × T) : ((NonUnitalRingHom.fst S T).comp f).prod ((NonUnitalRingHom.snd S T).comp f) = f
• NonUnitalRingHom.prod_apply 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) : (f.prod g) x = (f x, g x)
• NonUnitalRingHom.prodMap_def 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') : f.prodMap g = (f.comp (NonUnitalRingHom.fst R S)).prod (g.comp (NonUnitalRingHom.snd R S))
• NonUnitalRingHom.prod_comp_prodMap 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] [NonUnitalNonAssocSemiring T] (f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S') : (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
• NonUnitalRingHom.coe_prodMap 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• NonUnitalSubsemiring.map_id 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) : NonUnitalSubsemiring.map (NonUnitalRingHom.id R) s = s
• NonUnitalSubsemiring.range_fst 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : NonUnitalRingHom.srange (NonUnitalRingHom.fst R S) = ⊤
• NonUnitalSubsemiring.range_snd 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : NonUnitalRingHom.srange (NonUnitalRingHom.snd R S) = ⊤
• NonUnitalRingHom.srangeRestrict 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] (f : F) : R →ₙ+* ↥(NonUnitalRingHom.srange f)
• NonUnitalSubsemiring.prod_top 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (s : NonUnitalSubsemiring R) : s.prod ⊤ = NonUnitalSubsemiring.comap (NonUnitalRingHom.fst R S) s
• NonUnitalSubsemiring.top_prod 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (s : NonUnitalSubsemiring S) : ⊤.prod s = NonUnitalSubsemiring.comap (NonUnitalRingHom.snd R S) s
• NonUnitalRingHom.map_srange 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} {T : Type w} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (g : S →ₙ+* T) (f : R →ₙ+* S) : NonUnitalSubsemiring.map g (NonUnitalRingHom.srange f) = NonUnitalRingHom.srange (g.comp f)
• NonUnitalSubsemiring.comap_comap 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} {T : Type w} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] {F : Type u_1} {G : Type u_2} [FunLike F R S] [NonUnitalRingHomClass F R S] [FunLike G S T] [NonUnitalRingHomClass G S T] (s : NonUnitalSubsemiring T) (g : G) (f : F) : NonUnitalSubsemiring.comap f (NonUnitalSubsemiring.comap g s) = NonUnitalSubsemiring.comap ((↑g).comp ↑f) s
• NonUnitalSubsemiring.map_map 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} {T : Type w} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] {F : Type u_1} {G : Type u_2} [FunLike F R S] [NonUnitalRingHomClass F R S] [FunLike G S T] [NonUnitalRingHomClass G S T] (s : NonUnitalSubsemiring R) (g : G) (f : F) : NonUnitalSubsemiring.map (↑g) (NonUnitalSubsemiring.map (↑f) s) = NonUnitalSubsemiring.map ((↑g).comp ↑f) s
• NonUnitalSubsemiring.srange_subtype 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) : NonUnitalRingHom.srange (NonUnitalSubsemiringClass.subtype s) = s
• NonUnitalRingHom.srangeRestrict_surjective 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] (f : F) : Function.Surjective ⇑(NonUnitalRingHom.srangeRestrict f)
• NonUnitalRingHom.coe_srangeRestrict 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] (f : F) (x : R) : ↑((NonUnitalRingHom.srangeRestrict f) x) = f x
• NonUnitalSubsemiring.mem_map_equiv 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {f : R ≃+* S} {K : NonUnitalSubsemiring R} {x : S} : x ∈ NonUnitalSubsemiring.map (↑f) K ↔ f.symm x ∈ K
• NonUnitalSubsemiring.comap_equiv_eq_map_symm 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) (K : NonUnitalSubsemiring S) : NonUnitalSubsemiring.comap (↑f) K = NonUnitalSubsemiring.map f.symm K
• NonUnitalSubsemiring.map_equiv_eq_comap_symm 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) (K : NonUnitalSubsemiring R) : NonUnitalSubsemiring.map (↑f) K = NonUnitalSubsemiring.comap f.symm K
• RingEquiv.nonUnitalSubsemiringMap 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : NonUnitalSubsemiring R) : ↥s ≃+* ↥(NonUnitalSubsemiring.map e.toNonUnitalRingHom s)
• RingEquiv.nonUnitalSubsemiringMap_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : NonUnitalSubsemiring R) (x : ↑↑s.toAddSubmonoid) : ↑((e.nonUnitalSubsemiringMap s) x) = e ↑x
• RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : NonUnitalSubsemiring R) (y : ↑(⇑↑e.toAddEquiv '' ↑s.toAddSubmonoid)) : ↑((e.nonUnitalSubsemiringMap s).symm y) = e.symm ↑y
• NonUnitalRingHom.range 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : NonUnitalSubring S
• NonUnitalRingHom.eqLocus 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f g : R →ₙ+* S) : NonUnitalSubring R
• NonUnitalRingHom.eqLocus_same 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : f.eqLocus f = ⊤
• NonUnitalRingHom.fintypeRange 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [Fintype R] [DecidableEq S] (f : R →ₙ+* S) : Fintype ↥f.range
• NonUnitalSubring.map_id 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) : NonUnitalSubring.map (NonUnitalRingHom.id R) s = s
• NonUnitalRingHom.coe_range 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : ↑f.range = Set.range ⇑f
• NonUnitalRingHom.range_eq_top_of_surjective 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (hf : Function.Surjective ⇑f) : f.range = ⊤
• NonUnitalRingHom.mem_range_self 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (x : R) : f x ∈ f.range
• NonUnitalRingHom.range_eq_top 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f : R →ₙ+* S} : f.range = ⊤ ↔ Function.Surjective ⇑f
• NonUnitalRingHom.range_eq_map 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : f.range = NonUnitalSubring.map f ⊤
• NonUnitalSubring.comap_top 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : NonUnitalSubring.comap f ⊤ = ⊤
• NonUnitalSubring.map_bot 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : NonUnitalSubring.map f ⊥ = ⊥
• NonUnitalRingHom.mem_range 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f : R →ₙ+* S} {y : S} : y ∈ f.range ↔ ∃ x, f x = y
• NonUnitalRingHom.rangeRestrict 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : R →ₙ+* ↥f.range
• NonUnitalRingHom.map_closure 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (s : Set R) : NonUnitalSubring.map f (NonUnitalSubring.closure s) = NonUnitalSubring.closure (⇑f '' s)
• NonUnitalRingHom.map_range 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} {T : Type u_1} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [NonUnitalNonAssocRing T] (g : S →ₙ+* T) (f : R →ₙ+* S) : NonUnitalSubring.map g f.range = (g.comp f).range
• NonUnitalRingHom.mem_eqLocus 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f g : R →ₙ+* S} {x : R} : x ∈ f.eqLocus g ↔ f x = g x
• NonUnitalRingHom.closure_preimage_le 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (s : Set S) : NonUnitalSubring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubring.comap f (NonUnitalSubring.closure s)
• NonUnitalRingHom.eq_of_eqOn_set_top 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f g : R →ₙ+* S} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g
• NonUnitalSubring.range_fst 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : NonUnitalRingHom.srange (NonUnitalRingHom.fst R S) = ⊤
• NonUnitalSubring.range_snd 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : NonUnitalRingHom.srange (NonUnitalRingHom.snd R S) = ⊤
• NonUnitalRingHom.eq_of_eqOn_set_dense 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {s : Set R} (hs : NonUnitalSubring.closure s = ⊤) {f g : R →ₙ+* S} (h : Set.EqOn (⇑f) (⇑g) s) : f = g
• NonUnitalSubring.prod_top 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (s : NonUnitalSubring R) : s.prod ⊤ = NonUnitalSubring.comap (NonUnitalRingHom.fst R S) s
• NonUnitalSubring.top_prod 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (s : NonUnitalSubring S) : ⊤.prod s = NonUnitalSubring.comap (NonUnitalRingHom.snd R S) s
• NonUnitalRingHom.eqOn_set_closure 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f g : R →ₙ+* S} {s : Set R} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(NonUnitalSubring.closure s)
• NonUnitalSubring.comap_comap 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} {T : Type u_1} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [NonUnitalNonAssocRing T] (s : NonUnitalSubring T) (g : S →ₙ+* T) (f : R →ₙ+* S) : NonUnitalSubring.comap f (NonUnitalSubring.comap g s) = NonUnitalSubring.comap (g.comp f) s
• NonUnitalSubring.map_map 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} {T : Type u_1} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [NonUnitalNonAssocRing T] (s : NonUnitalSubring R) (g : S →ₙ+* T) (f : R →ₙ+* S) : NonUnitalSubring.map g (NonUnitalSubring.map f s) = NonUnitalSubring.map (g.comp f) s
• NonUnitalRingHom.rangeRestrict_surjective 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) : Function.Surjective ⇑f.rangeRestrict
• NonUnitalRingHom.coe_rangeRestrict 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R →ₙ+* S) (x : R) : ↑(f.rangeRestrict x) = f x
• RingEquiv.ofLeftInverse' 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalRing R] [NonUnitalRing S] {g : S → R} {f : R →ₙ+* S} (h : Function.LeftInverse g ⇑f) : R ≃+* ↥f.range
• NonUnitalSubring.mem_map_equiv 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {f : R ≃+* S} {K : NonUnitalSubring R} {x : S} : x ∈ NonUnitalSubring.map (↑f) K ↔ f.symm x ∈ K
• NonUnitalSubring.comap_equiv_eq_map_symm 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R ≃+* S) (K : NonUnitalSubring S) : NonUnitalSubring.comap (↑f) K = NonUnitalSubring.map f.symm K
• NonUnitalSubring.map_equiv_eq_comap_symm 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R ≃+* S) (K : NonUnitalSubring R) : NonUnitalSubring.map (↑f) K = NonUnitalSubring.comap f.symm K
• RingEquiv.ofLeftInverse'_apply 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalRing R] [NonUnitalRing S] {g : S → R} {f : R →ₙ+* S} (h : Function.LeftInverse g ⇑f) (x : R) : ↑((RingEquiv.ofLeftInverse' h) x) = f x
• RingEquiv.ofLeftInverse'_symm_apply 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} {S : Type v} [NonUnitalRing R] [NonUnitalRing S] {g : S → R} {f : R →ₙ+* S} (h : Function.LeftInverse g ⇑f) (x : ↥f.range) : (RingEquiv.ofLeftInverse' h).symm x = g ↑x
• RingCon.comap_nonUnitalRingHomId 📋 Mathlib.RingTheory.Congruence.Defs
  {R : Type u_5} [NonUnitalNonAssocSemiring R] (J : RingCon R) : J.comap (NonUnitalRingHom.id R) = J
• RingCon.comap_nonUnitalRingHomComp 📋 Mathlib.RingTheory.Congruence.Defs
  {R : Type u_5} {R' : Type u_6} {R'' : Type u_7} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring R''] (J : RingCon R) (g : R' →ₙ+* R) (f : R'' →ₙ+* R') : J.comap (g.comp f) = (J.comap g).comap f
• AddMonoidAlgebra.mapDomainNonUnitalRingHom 📋 Mathlib.Algebra.MonoidAlgebra.MapDomain
  (R : Type u_3) {M : Type u_6} {N : Type u_7} [Semiring R] [Add M] [Add N] (f : M →ₙ+ N) : AddMonoidAlgebra R M →ₙ+* AddMonoidAlgebra R N
• MonoidAlgebra.mapDomainNonUnitalRingHom 📋 Mathlib.Algebra.MonoidAlgebra.MapDomain
  (R : Type u_3) {M : Type u_6} {N : Type u_7} [Semiring R] [Mul M] [Mul N] (f : M →ₙ* N) : MonoidAlgebra R M →ₙ+* MonoidAlgebra R N
• AddMonoidAlgebra.mapDomainNonUnitalRingHom_id 📋 Mathlib.Algebra.MonoidAlgebra.MapDomain
  {R : Type u_3} {M : Type u_6} [Semiring R] [Add M] : AddMonoidAlgebra.mapDomainNonUnitalRingHom R (AddHom.id M) = NonUnitalRingHom.id (AddMonoidAlgebra R M)
• MonoidAlgebra.mapDomainNonUnitalRingHom_id 📋 Mathlib.Algebra.MonoidAlgebra.MapDomain
  {R : Type u_3} {M : Type u_6} [Semiring R] [Mul M] : MonoidAlgebra.mapDomainNonUnitalRingHom R (MulHom.id M) = NonUnitalRingHom.id (MonoidAlgebra R M)
• AddMonoidAlgebra.mapDomainNonUnitalRingHom_comp 📋 Mathlib.Algebra.MonoidAlgebra.MapDomain
  {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [Semiring R] [Add M] [Add N] [Add O] (f : N →ₙ+ O) (g : M →ₙ+ N) : AddMonoidAlgebra.mapDomainNonUnitalRingHom R (f.comp g) = (AddMonoidAlgebra.mapDomainNonUnitalRingHom R f).comp (AddMonoidAlgebra.mapDomainNonUnitalRingHom R g)
• MonoidAlgebra.mapDomainNonUnitalRingHom_comp 📋 Mathlib.Algebra.MonoidAlgebra.MapDomain
  {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [Semiring R] [Mul M] [Mul N] [Mul O] (f : N →ₙ* O) (g : M →ₙ* N) : MonoidAlgebra.mapDomainNonUnitalRingHom R (f.comp g) = (MonoidAlgebra.mapDomainNonUnitalRingHom R f).comp (MonoidAlgebra.mapDomainNonUnitalRingHom R g)
• AddMonoidAlgebra.mapDomainNonUnitalRingHom_apply 📋 Mathlib.Algebra.MonoidAlgebra.MapDomain
  (R : Type u_3) {M : Type u_6} {N : Type u_7} [Semiring R] [Add M] [Add N] (f : M →ₙ+ N) (x : AddMonoidAlgebra R M) : (AddMonoidAlgebra.mapDomainNonUnitalRingHom R f) x = AddMonoidAlgebra.mapDomain (⇑f) x
• MonoidAlgebra.mapDomainNonUnitalRingHom_apply 📋 Mathlib.Algebra.MonoidAlgebra.MapDomain
  (R : Type u_3) {M : Type u_6} {N : Type u_7} [Semiring R] [Mul M] [Mul N] (f : M →ₙ* N) (x : MonoidAlgebra R M) : (MonoidAlgebra.mapDomainNonUnitalRingHom R f) x = MonoidAlgebra.mapDomain (⇑f) x
• NonUnitalAlgHom.coe_restrictScalars 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₙₐ[S] B) : ↑(NonUnitalAlgHom.restrictScalars R f) = ↑f
• NonUnitalSubalgebra.map_toNonUnitalSubsemiring 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (NonUnitalSubalgebra.map f S).toNonUnitalSubsemiring = NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring
• NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} : NonUnitalSubsemiringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)
• NonUnitalSubalgebra.toSubring_subtype 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)
• NonUnitalStarRingHom.toNonUnitalRingHom 📋 Mathlib.Algebra.Star.StarRingHom
  {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (self : A →⋆ₙ+* B) : A →ₙ+* B
• NonUnitalStarRingHom.coe_toNonUnitalRingHom 📋 Mathlib.Algebra.Star.StarRingHom
  {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →⋆ₙ+* B) : ⇑f.toNonUnitalRingHom = ⇑f
• NonUnitalStarRingHom.mk 📋 Mathlib.Algebra.Star.StarRingHom
  {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (toNonUnitalRingHom : A →ₙ+* B) (map_star' : ∀ (a : A), toNonUnitalRingHom.toFun (star a) = star (toNonUnitalRingHom.toFun a)) : A →⋆ₙ+* B
• NonUnitalStarRingHom.coe_mk 📋 Mathlib.Algebra.Star.StarRingHom
  {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Star A] [NonUnitalNonAssocSemiring B] [Star B] (f : A →ₙ+* B) (h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)) : ⇑{ toNonUnitalRingHom := f, map_star' := h } = ⇑f
• NonUnitalStarAlgHom.coe_restrictScalars 📋 Mathlib.Algebra.Star.StarAlgHom
  (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [Star A] [Star B] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →⋆ₙₐ[S] B) : ↑(NonUnitalStarAlgHom.restrictScalars R f) = ↑f
• NonUnitalStarSubalgebra.toSubring_subtype 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [Star A] (S : NonUnitalStarSubalgebra R A) : NonUnitalSubringClass.subtype S = ↑(NonUnitalStarSubalgebraClass.subtype S)
• DirectLimit.NonUnitalRing.of 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (i : ι) : G i →ₙ+* DirectLimit G f
• DirectLimit.NonUnitalRing.lift 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] (g : (i : ι) → G i →ₙ+* P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) : DirectLimit G f →ₙ+* P
• DirectLimit.NonUnitalRing.of_apply 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (i : ι) (x : G i) : (DirectLimit.NonUnitalRing.of G f i) x = ⟦⟨i, x⟩⟧
• DirectLimit.NonUnitalRing.lift_comp_of 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] (g : (i : ι) → G i →ₙ+* P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι} : (DirectLimit.NonUnitalRing.lift G f P g Hg).comp (DirectLimit.NonUnitalRing.of G f i) = g i
• DirectLimit.NonUnitalRing.hom_ext 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] {g₁ g₂ : DirectLimit G f →ₙ+* P} (h : ∀ (i : ι), g₁.comp (DirectLimit.NonUnitalRing.of G f i) = g₂.comp (DirectLimit.NonUnitalRing.of G f i)) : g₁ = g₂
• DirectLimit.NonUnitalRing.hom_ext_iff 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] {P : Type u_7} [NonUnitalNonAssocSemiring P] {g₁ g₂ : DirectLimit G f →ₙ+* P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (DirectLimit.NonUnitalRing.of G f i) = g₂.comp (DirectLimit.NonUnitalRing.of G f i)
• DirectLimit.NonUnitalRing.of_f 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] {i j : ι} (hij : i ≤ j) (x : G i) : (DirectLimit.NonUnitalRing.of G f j) ((f i j hij) x) = (DirectLimit.NonUnitalRing.of G f i) x
• DirectLimit.NonUnitalRing.lift_apply 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] (g : (i : ι) → G i →ₙ+* P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (z : DirectLimit G f) : (DirectLimit.NonUnitalRing.lift G f P g Hg) z = DirectLimit.lift f (fun x1 x2 => (g x1) x2) ⋯ z
• DirectLimit.NonUnitalRing.lift_of 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] (g : (i : ι) → G i →ₙ+* P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι) (x : G i) : (DirectLimit.NonUnitalRing.lift G f P g Hg) ((DirectLimit.NonUnitalRing.of G f i) x) = (g i) x
• HahnSeries.map_mul 📋 Mathlib.RingTheory.HahnSeries.Multiplication
  {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) {x y : HahnSeries Γ R} : (x * y).map f = x.map f * y.map f
• CentroidHom.centerToCentroid 📋 Mathlib.Algebra.Ring.CentroidHom
  {α : Type u_5} [NonUnitalNonAssocSemiring α] : ↥(NonUnitalSubsemiring.center α) →ₙ+* CentroidHom α
• CentroidHom.centerToCentroidCenter 📋 Mathlib.Algebra.Ring.CentroidHom
  {α : Type u_5} [NonUnitalNonAssocSemiring α] : ↥(NonUnitalSubsemiring.center α) →ₙ+* ↥(Subsemiring.center (CentroidHom α))
• CentroidHom.centerToCentroid_apply 📋 Mathlib.Algebra.Ring.CentroidHom
  {α : Type u_5} [NonUnitalNonAssocSemiring α] (z : ↥(NonUnitalSubsemiring.center α)) (a : α) : (CentroidHom.centerToCentroid z) a = ↑z * a
• CentroidHom.centerToCentroidCenter_apply 📋 Mathlib.Algebra.Ring.CentroidHom
  {α : Type u_5} [NonUnitalNonAssocSemiring α] (z : ↥(NonUnitalSubsemiring.center α)) (a : α) : (CentroidHom.centerToCentroidCenter z) a = ↑z * a

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