Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Damiano Testa

! This file was ported from Lean 3 source module algebra.smul_with_zero
! leanprover-community/mathlib commit 966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupPower.Basic
import Mathlib.Algebra.Ring.Opposite
import Mathlib.GroupTheory.GroupAction.Opposite
import Mathlib.GroupTheory.GroupAction.Prod

/-!
# Introduce `SMulWithZero`

In analogy with the usual monoid action on a Type `M`, we introduce an action of a
`MonoidWithZero` on a Type with `0`.

In particular, for Types `R` and `M`, both containing `0`, we define `SMulWithZero R M` to
be the typeclass where the products `r • 0` and `0 • m` vanish for all `r : R` and all `m : M`.

Moreover, in the case in which `R` is a `MonoidWithZero`, we introduce the typeclass
`MulActionWithZero R M`, mimicking group actions and having an absorbing `0` in `R`.
Thus, the action is required to be compatible with

* the unit of the monoid, acting as the identity;
* the zero of the `MonoidWithZero`, acting as zero;
* associativity of the monoid.

* any `MonoidWithZero` has a `MulActionWithZero R R` acting on itself.

## Main declarations

* `smulMonoidWithZeroHom`: Scalar multiplication bundled as a morphism of monoids with zero.
-/

variable {R: Type ?u.16491R R': Type ?u.17R' M: Type ?u.20M M': Type ?u.3539M' : Type _: Type (?u.23+1)Type _}

section Zero

variable (R: ?m.26R M: ?m.29M)

/-- `SMulWithZero` is a class consisting of a Type `R` with `0 ∈ R` and a scalar multiplication
of `R` on a Type `M` with `0`, such that the equality `r • m = 0` holds if at least one among `r`
or `m` equals `0`. -/
class SMulWithZero: (R : Type u_1) → (M : Type u_2) → [inst : Zero R] → [inst : Zero M] → Type (maxu_1u_2)SMulWithZero [Zero: Type ?u.44 → Type ?u.44Zero R: Type ?u.32R] [Zero: Type ?u.47 → Type ?u.47Zero M: Type ?u.38M] extends SMulZeroClass: Type ?u.53 → (A : Type ?u.52) → [inst : Zero A] → Type (max?u.53?u.52)SMulZeroClass R: Type ?u.32R M: Type ?u.38M where
/-- Scalar multiplication by the scalar `0` is `0`. -/
zero_smul: ∀ {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst_1 : Zero M] [self : SMulWithZero R M] (m : M), 0 • m = 0zero_smul : ∀ m: Mm : M: Type ?u.38M, (0: ?m.880 : R: Type ?u.32R) • m: Mm = 0: ?m.1410
#align smul_with_zero SMulWithZero: (R : Type u_1) → (M : Type u_2) → [inst : Zero R] → [inst : Zero M] → Type (maxu_1u_2)SMulWithZero

instance MulZeroClass.toSMulWithZero: [inst : MulZeroClass R] → SMulWithZero R RMulZeroClass.toSMulWithZero [MulZeroClass: Type ?u.235 → Type ?u.235MulZeroClass R: Type ?u.223R] : SMulWithZero: (R : Type ?u.239) → (M : Type ?u.238) → [inst : Zero R] → [inst : Zero M] → Type (max?u.239?u.238)SMulWithZero R: Type ?u.223R R: Type ?u.223R where
smul := (· * ·): R → R → R(· * ·)
smul_zero := mul_zero: ∀ {M₀ : Type ?u.757} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0mul_zero
zero_smul := zero_mul: ∀ {M₀ : Type ?u.794} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0zero_mul
#align mul_zero_class.to_smul_with_zero MulZeroClass.toSMulWithZero: (R : Type u_1) → [inst : MulZeroClass R] → SMulWithZero R RMulZeroClass.toSMulWithZero

/-- Like `MulZeroClass.toSMulWithZero`, but multiplies on the right. -/
instance MulZeroClass.toOppositeSMulWithZero: (R : Type u_1) → [inst : MulZeroClass R] → SMulWithZero Rᵐᵒᵖ RMulZeroClass.toOppositeSMulWithZero [MulZeroClass: Type ?u.920 → Type ?u.920MulZeroClass R: Type ?u.908R] : SMulWithZero: (R : Type ?u.924) → (M : Type ?u.923) → [inst : Zero R] → [inst : Zero M] → Type (max?u.924?u.923)SMulWithZero R: Type ?u.908Rᵐᵒᵖ R: Type ?u.908R where
smul := (· • ·): Rᵐᵒᵖ → R → R(· • ·)
smul_zero _: ?m.1628_ := zero_mul: ∀ {M₀ : Type ?u.1630} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0zero_mul _: ?m.1631_
zero_smul := mul_zero: ∀ {M₀ : Type ?u.1667} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0mul_zero
#align mul_zero_class.to_opposite_smul_with_zero MulZeroClass.toOppositeSMulWithZero: (R : Type u_1) → [inst : MulZeroClass R] → SMulWithZero Rᵐᵒᵖ RMulZeroClass.toOppositeSMulWithZero

variable {M: ?m.1773M} [Zero: Type ?u.2224 → Type ?u.2224Zero R: Type ?u.1761R] [Zero: Type ?u.3242 → Type ?u.3242Zero M: Type ?u.3233M] [SMulWithZero: (R : Type ?u.3246) → (M : Type ?u.3245) → [inst : Zero R] → [inst : Zero M] → Type (max?u.3246?u.3245)SMulWithZero R: Type ?u.1761R M: ?m.1773M]

@[simp]
theorem zero_smul: ∀ (R : Type u_2) {M : Type u_1} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (m : M), 0 • m = 0zero_smul (m: Mm : M: Type ?u.1821M) : (0: ?m.18800 : R: Type ?u.1815R) • m: Mm = 0: ?m.19880 :=
SMulWithZero.zero_smul: ∀ {R : Type ?u.2027} {M : Type ?u.2026} [inst : Zero R] [inst_1 : Zero M] [self : SMulWithZero R M] (m : M), 0 • m = 0SMulWithZero.zero_smul m: Mm
#align zero_smul zero_smul: ∀ (R : Type u_2) {M : Type u_1} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (m : M), 0 • m = 0zero_smul

variable {R: ?m.2205R} {a: Ra : R: Type ?u.2212R} {b: Mb : M: Type ?u.2946M}

lemma smul_eq_zero_of_left: ∀ {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {a : R},
a = 0 → ∀ (b : M), a • b = 0smul_eq_zero_of_left (h: a = 0h : a: Ra = 0: ?m.22700) (b: Mb : M: Type ?u.2218M) : a: Ra • b: Mb = 0: ?m.24050 := h: a = 0h.symm: ∀ {α : Sort ?u.2444} {a b : α}, a = b → b = asymm ▸ zero_smul: ∀ (R : Type ?u.2456) {M : Type ?u.2455} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (m : M), 0 • m = 0zero_smul _: Type ?u.2456_ b: Mb
#align smul_eq_zero_of_left smul_eq_zero_of_left: ∀ {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {a : R},
a = 0 → ∀ (b : M), a • b = 0smul_eq_zero_of_left
lemma smul_eq_zero_of_right: ∀ (a : R), b = 0 → a • b = 0smul_eq_zero_of_right (a: Ra : R: Type ?u.2577R) (h: b = 0h : b: Mb = 0: ?m.26370) : a: Ra • b: Mb = 0: ?m.27700 := h: b = 0h.symm: ∀ {α : Sort ?u.2789} {a b : α}, a = b → b = asymm ▸ smul_zero: ∀ {M : Type ?u.2801} {A : Type ?u.2800} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0smul_zero a: Ra
#align smul_eq_zero_of_right smul_eq_zero_of_right: ∀ {R : Type u_2} {M : Type u_1} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {b : M} (a : R),
b = 0 → a • b = 0smul_eq_zero_of_right
lemma left_ne_zero_of_smul: ∀ {R : Type u_2} {M : Type u_1} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {a : R} {b : M},
a • b ≠ 0 → a ≠ 0left_ne_zero_of_smul : a: Ra • b: Mb ≠ 0: ?m.30930 → a: Ra ≠ 0: ?m.31190 := mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬amt \$ fun h: ?m.3150h ↦ smul_eq_zero_of_left: ∀ {R : Type ?u.3152} {M : Type ?u.3153} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {a : R},
a = 0 → ∀ (b : M), a • b = 0smul_eq_zero_of_left h: ?m.3150h b: Mb
#align left_ne_zero_of_smul left_ne_zero_of_smul: ∀ {R : Type u_2} {M : Type u_1} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {a : R} {b : M},
a • b ≠ 0 → a ≠ 0left_ne_zero_of_smul
lemma right_ne_zero_of_smul: ∀ {R : Type u_2} {M : Type u_1} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {a : R} {b : M},
a • b ≠ 0 → b ≠ 0right_ne_zero_of_smul : a: Ra • b: Mb ≠ 0: ?m.33800 → b: Mb ≠ 0: ?m.34060 := mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬amt \$ smul_eq_zero_of_right: ∀ {R : Type ?u.3417} {M : Type ?u.3416} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {b : M} (a : R),
b = 0 → a • b = 0smul_eq_zero_of_right a: Ra
#align right_ne_zero_of_smul right_ne_zero_of_smul: ∀ {R : Type u_2} {M : Type u_1} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] {a : R} {b : M},
a • b ≠ 0 → b ≠ 0right_ne_zero_of_smul

variable [Zero: Type ?u.3652 → Type ?u.3652Zero R': Type ?u.3533R'] [Zero: Type ?u.7974 → Type ?u.7974Zero M': Type ?u.3539M'] [SMul: Type ?u.11659 → Type ?u.11658 → Type (max?u.11659?u.11658)SMul R: Type ?u.3596R M': Type ?u.7924M']

/-- Pullback a `SMulWithZero` structure along an injective zero-preserving homomorphism.
See note [reducible non-instances]. -/
@[reducible]
protected def Function.Injective.smulWithZero: {R : Type u_1} →
{M : Type u_2} →
{M' : Type u_3} →
[inst : Zero R] →
[inst_1 : Zero M] →
[inst_2 : SMulWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M' M) → Injective ↑f → (∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b) → SMulWithZero R M'Function.Injective.smulWithZero (f: ZeroHom M' Mf : ZeroHom: (M : Type ?u.3663) → (N : Type ?u.3662) → [inst : Zero M] → [inst : Zero N] → Type (max?u.3663?u.3662)ZeroHom M': Type ?u.3605M' M: Type ?u.3602M) (hf: Injective ↑fhf : Function.Injective: {α : Sort ?u.3697} → {β : Sort ?u.3696} → (α → β) → PropFunction.Injective f: ZeroHom M' Mf)
(smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f bsmul : ∀ (a: Ra : R: Type ?u.3596R) (b: ?m.4495b), f: ZeroHom M' Mf (a: Ra • b: ?m.4495b) = a: Ra • f: ZeroHom M' Mf b: ?m.4495b) :
SMulWithZero: (R : Type ?u.6309) → (M : Type ?u.6308) → [inst : Zero R] → [inst : Zero M] → Type (max?u.6309?u.6308)SMulWithZero R: Type ?u.3596R M': Type ?u.3605M' where
smul := (· • ·): R → M' → M'(· • ·)
zero_smul a: ?m.6399a := hf: Injective ↑fhf <| byGoals accomplished! 🐙 R: Type ?u.3596R': Type ?u.3599M: Type ?u.3602M': Type ?u.3605inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma✝: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M' Mhf: Injective ↑fsmul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f ba: M'↑f (0 • a) = ↑f 0simp [smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f bsmul]Goals accomplished! 🐙
smul_zero a: ?m.6387a := hf: Injective ↑fhf <| byGoals accomplished! 🐙 R: Type ?u.3596R': Type ?u.3599M: Type ?u.3602M': Type ?u.3605inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma✝: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M' Mhf: Injective ↑fsmul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f ba: R↑f (a • 0) = ↑f 0simp [smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f bsmul]Goals accomplished! 🐙
#align function.injective.smul_with_zero Function.Injective.smulWithZero: {R : Type u_1} →
{M : Type u_2} →
{M' : Type u_3} →
[inst : Zero R] →
[inst_1 : Zero M] →
[inst_2 : SMulWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M' M) →
Function.Injective ↑f → (∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b) → SMulWithZero R M'Function.Injective.smulWithZero

/-- Pushforward a `SMulWithZero` structure along a surjective zero-preserving homomorphism.
See note [reducible non-instances]. -/
@[reducible]
protected def Function.Surjective.smulWithZero: {R : Type u_1} →
{M : Type u_2} →
{M' : Type u_3} →
[inst : Zero R] →
[inst_1 : Zero M] →
[inst_2 : SMulWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M M') → Surjective ↑f → (∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b) → SMulWithZero R M'Function.Surjective.smulWithZero (f: ZeroHom M M'f : ZeroHom: (M : Type ?u.7982) → (N : Type ?u.7981) → [inst : Zero M] → [inst : Zero N] → Type (max?u.7982?u.7981)ZeroHom M: Type ?u.7921M M': Type ?u.7924M') (hf: Surjective ↑fhf : Function.Surjective: {α : Sort ?u.8016} → {β : Sort ?u.8015} → (α → β) → PropFunction.Surjective f: ZeroHom M M'f)
(smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bsmul : ∀ (a: Ra : R: Type ?u.7915R) (b: ?m.8820b), f: ZeroHom M M'f (a: Ra • b: ?m.8820b) = a: Ra • f: ZeroHom M M'f b: ?m.8820b) :
SMulWithZero: (R : Type ?u.10630) → (M : Type ?u.10629) → [inst : Zero R] → [inst : Zero M] → Type (max?u.10630?u.10629)SMulWithZero R: Type ?u.7915R M': Type ?u.7924M' where
smul := (· • ·): R → M' → M'(· • ·)
zero_smul m: ?m.10719m := byGoals accomplished! 🐙
R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bm: M'0 • m = 0rcases hf: Surjective ↑fhf m: M'm with ⟨x, rfl⟩: ∃ a, ↑f a = m⟨x: Mx⟨x, rfl⟩: ∃ a, ↑f a = m, rfl: ↑f x = mrfl⟨x, rfl⟩: ∃ a, ↑f a = m⟩R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bx: Mintro0 • ↑f x = 0
R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bm: M'0 • m = 0simp [← smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bsmul]Goals accomplished! 🐙
smul_zero c: ?m.10709c := byGoals accomplished! 🐙 R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bc: Rc • 0 = 0rw [R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bc: Rc • 0 = 0←f: ZeroHom M M'f.map_zero: ∀ {M : Type ?u.10728} {N : Type ?u.10729} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N), ↑f 0 = 0map_zero,R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bc: Rc • ↑f 0 = ↑f 0 R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bc: Rc • 0 = 0←smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bsmul,R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bc: R↑f (c • 0) = ↑f 0 R: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bc: Rc • 0 = 0smul_zero: ∀ {M : Type ?u.10801} {A : Type ?u.10800} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0smul_zeroR: Type ?u.7915R': Type ?u.7918M: Type ?u.7921M': Type ?u.7924inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom M M'hf: Surjective ↑fsmul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bc: R↑f 0 = ↑f 0]Goals accomplished! 🐙
#align function.surjective.smul_with_zero Function.Surjective.smulWithZero: {R : Type u_1} →
{M : Type u_2} →
{M' : Type u_3} →
[inst : Zero R] →
[inst_1 : Zero M] →
[inst_2 : SMulWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M M') →
Function.Surjective ↑f → (∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b) → SMulWithZero R M'Function.Surjective.smulWithZero

variable (M: ?m.11662M)

/-- Compose a `SMulWithZero` with a `ZeroHom`, with action `f r' • m` -/
def SMulWithZero.compHom: {R : Type u_1} →
{R' : Type u_2} →
(M : Type u_3) →
[inst : Zero R] →
[inst_1 : Zero M] → [inst_2 : SMulWithZero R M] → [inst_3 : Zero R'] → ZeroHom R' R → SMulWithZero R' MSMulWithZero.compHom (f: ZeroHom R' Rf : ZeroHom: (M : Type ?u.11732) → (N : Type ?u.11731) → [inst : Zero M] → [inst : Zero N] → Type (max?u.11732?u.11731)ZeroHom R': Type ?u.11668R' R: Type ?u.11665R) : SMulWithZero: (R : Type ?u.11766) → (M : Type ?u.11765) → [inst : Zero R] → [inst : Zero M] → Type (max?u.11766?u.11765)SMulWithZero R': Type ?u.11668R' M: Type ?u.11671M where
smul := (· • ·): R → M → M(· • ·) ∘ f: ZeroHom R' Rf
smul_zero m: ?m.12705m := smul_zero: ∀ {M : Type ?u.12708} {A : Type ?u.12707} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0smul_zero (f: ZeroHom R' Rf m: ?m.12705m)
zero_smul m: ?m.13667m := byGoals accomplished! 🐙 R: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M0 • m = 0show (f: ZeroHom R' Rf 0: ?m.144530) • m: Mm = 0: ?m.145390R: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M↑f 0 • m = 0 R: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M0 • m = 0;R: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M↑f 0 • m = 0 R: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M0 • m = 0rw [R: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M↑f 0 • m = 0map_zero: ∀ {M : Type ?u.14587} {N : Type ?u.14588} {F : Type ?u.14586} [inst : Zero M] [inst_1 : Zero N]
[inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0map_zero,R: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M0 • m = 0 R: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M↑f 0 • m = 0zero_smul: ∀ {R : Type ?u.14836} {M : Type ?u.14835} [inst : Zero R] [inst_1 : Zero M] [self : SMulWithZero R M] (m : M), 0 • m = 0zero_smulR: Type ?u.11665R': Type ?u.11668M: Type ?u.11671M': Type ?u.11674inst✝⁵: Zero Rinst✝⁴: Zero Minst✝³: SMulWithZero R Ma: Rb: Minst✝²: Zero R'inst✝¹: Zero M'inst✝: SMul R M'f: ZeroHom R' Rm: M0 = 0]Goals accomplished! 🐙
#align smul_with_zero.comp_hom SMulWithZero.compHom: {R : Type u_1} →
{R' : Type u_2} →
(M : Type u_3) →
[inst : Zero R] →
[inst_1 : Zero M] → [inst_2 : SMulWithZero R M] → [inst_3 : Zero R'] → ZeroHom R' R → SMulWithZero R' MSMulWithZero.compHom

end Zero

instance AddMonoid.natSMulWithZero: {M : Type u_1} → [inst : AddMonoid M] → SMulWithZero ℕ MAddMonoid.natSMulWithZero [AddMonoid: Type ?u.15205 → Type ?u.15205AddMonoid M: Type ?u.15199M] : SMulWithZero: (R : Type ?u.15209) → (M : Type ?u.15208) → [inst : Zero R] → [inst : Zero M] → Type (max?u.15209?u.15208)SMulWithZero ℕ: Typeℕ M: Type ?u.15199M where
smul_zero := _root_.nsmul_zero: ∀ {A : Type ?u.16371} [inst : AddMonoid A] (n : ℕ), n • 0 = 0_root_.nsmul_zero
zero_smul := zero_nsmul: ∀ {M : Type ?u.16414} [inst : AddMonoid M] (a : M), 0 • a = 0zero_nsmul

instance AddGroup.intSMulWithZero: {M : Type u_1} → [inst : AddGroup M] → SMulWithZero ℤ MAddGroup.intSMulWithZero [AddGroup: Type ?u.16503 → Type ?u.16503AddGroup M: Type ?u.16497M] : SMulWithZero: (R : Type ?u.16507) → (M : Type ?u.16506) → [inst : Zero R] → [inst : Zero M] → Type (max?u.16507?u.16506)SMulWithZero ℤ: Typeℤ M: Type ?u.16497M where
smul_zero := zsmul_zero: ∀ {α : Type ?u.17577} [inst : SubtractionMonoid α] (n : ℤ), n • 0 = 0zsmul_zero
zero_smul := zero_zsmul: ∀ {G : Type ?u.17673} [inst : SubNegMonoid G] (a : G), 0 • a = 0zero_zsmul

section MonoidWithZero

variable [MonoidWithZero: Type ?u.18447 → Type ?u.18447MonoidWithZero R: Type ?u.17760R] [MonoidWithZero: Type ?u.17775 → Type ?u.17775MonoidWithZero R': Type ?u.17763R'] [Zero: Type ?u.19385 → Type ?u.19385Zero M: Type ?u.17766M]

variable (R: ?m.17802R M: ?m.17805M)

/-- An action of a monoid with zero `R` on a Type `M`, also with `0`, extends `MulAction` and
is compatible with `0` (both in `R` and in `M`), with `1 ∈ R`, and with associativity of
multiplication on the monoid `M`. -/
class MulActionWithZero: (R : Type u_1) → (M : Type u_2) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (maxu_1u_2)MulActionWithZero extends MulAction: (α : Type ?u.17832) → Type ?u.17831 → [inst : Monoid α] → Type (max?u.17832?u.17831)MulAction R: Type ?u.17808R M: Type ?u.17814M where
-- these fields are copied from `SMulWithZero`, as `extends` behaves poorly
/-- Scalar multiplication by any element send `0` to `0`. -/
smul_zero: ∀ {R : Type u_1} {M : Type u_2} [inst : MonoidWithZero R] [inst_1 : Zero M] [self : MulActionWithZero R M] (r : R),
r • 0 = 0smul_zero : ∀ r: Rr : R: Type ?u.17808R, r: Rr • (0: ?m.178710 : M: Type ?u.17814M) = 0: ?m.179240
/-- Scalar multiplication by the scalar `0` is `0`. -/
zero_smul: ∀ {R : Type u_1} {M : Type u_2} [inst : MonoidWithZero R] [inst_1 : Zero M] [self : MulActionWithZero R M] (m : M),
0 • m = 0zero_smul : ∀ m: Mm : M: Type ?u.17814M, (0: ?m.179560 : R: Type ?u.17808R) • m: Mm = 0: ?m.180280
#align mul_action_with_zero MulActionWithZero: (R : Type u_1) → (M : Type u_2) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (maxu_1u_2)MulActionWithZero

-- see Note [lower instance priority]
instance (priority := 100) MulActionWithZero.toSMulWithZero: (R : Type u_1) →
(M : Type u_2) → [inst : MonoidWithZero R] → [inst_1 : Zero M] → [m : MulActionWithZero R M] → SMulWithZero R MMulActionWithZero.toSMulWithZero [m: MulActionWithZero R Mm : MulActionWithZero: (R : Type ?u.18124) → (M : Type ?u.18123) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.18124?u.18123)MulActionWithZero R: Type ?u.18102R M: Type ?u.18108M] :
SMulWithZero: (R : Type ?u.18151) → (M : Type ?u.18150) → [inst : Zero R] → [inst : Zero M] → Type (max?u.18151?u.18150)SMulWithZero R: Type ?u.18102R M: Type ?u.18108M :=
{ m: MulActionWithZero R Mm with }
#align mul_action_with_zero.to_smul_with_zero MulActionWithZero.toSMulWithZero: (R : Type u_1) →
(M : Type u_2) → [inst : MonoidWithZero R] → [inst_1 : Zero M] → [m : MulActionWithZero R M] → SMulWithZero R MMulActionWithZero.toSMulWithZero

instance MonoidWithZero.toMulActionWithZero: (R : Type u_1) → [inst : MonoidWithZero R] → MulActionWithZero R RMonoidWithZero.toMulActionWithZero : MulActionWithZero: (R : Type ?u.18457) → (M : Type ?u.18456) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.18457?u.18456)MulActionWithZero R: Type ?u.18435R R: Type ?u.18435R :=
{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651{ MulZeroClass.toSMulWithZero: (R : Type ?u.18514) → [inst : MulZeroClass R] → SMulWithZero R RMulZeroClass.toSMulWithZero{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651 R: Type ?u.18435R{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651, Monoid.toMulAction: (M : Type ?u.18628) → [inst : Monoid M] → MulAction M MMonoid.toMulAction{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651 R: Type ?u.18435R{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651 { MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651with{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651 }
#align monoid_with_zero.to_mul_action_with_zero MonoidWithZero.toMulActionWithZero: (R : Type u_1) → [inst : MonoidWithZero R] → MulActionWithZero R RMonoidWithZero.toMulActionWithZero

`Semiring.toOppositeModule` -/
instance MonoidWithZero.toOppositeMulActionWithZero: MulActionWithZero Rᵐᵒᵖ RMonoidWithZero.toOppositeMulActionWithZero : MulActionWithZero: (R : Type ?u.18873) → (M : Type ?u.18872) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.18873?u.18872)MulActionWithZero R: Type ?u.18851Rᵐᵒᵖ R: Type ?u.18851R :=
{ MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076{ MulZeroClass.toOppositeSMulWithZero: (R : Type ?u.18939) → [inst : MulZeroClass R] → SMulWithZero Rᵐᵒᵖ RMulZeroClass.toOppositeSMulWithZero{ MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076 R: Type ?u.18851R{ MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076, Monoid.toOppositeMulAction: (α : Type ?u.19053) → [inst : Monoid α] → MulAction αᵐᵒᵖ αMonoid.toOppositeMulAction{ MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076 R: Type ?u.18851R{ MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076 { MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076with{ MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076 }
#align monoid_with_zero.to_opposite_mul_action_with_zero MonoidWithZero.toOppositeMulActionWithZero: (R : Type u_1) → [inst : MonoidWithZero R] → MulActionWithZero Rᵐᵒᵖ RMonoidWithZero.toOppositeMulActionWithZero

protected lemma MulActionWithZero.subsingleton: ∀ (R : Type u_1) (M : Type u_2) [inst : MonoidWithZero R] [inst_1 : Zero M] [inst : MulActionWithZero R M]
[inst : Subsingleton R], Subsingleton MMulActionWithZero.subsingleton
[MulActionWithZero: (R : Type ?u.19389) → (M : Type ?u.19388) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.19389?u.19388)MulActionWithZero R: Type ?u.19367R M: Type ?u.19373M] [Subsingleton: Sort ?u.19415 → PropSubsingleton R: Type ?u.19367R] : Subsingleton: Sort ?u.19418 → PropSubsingleton M: Type ?u.19373M :=
⟨λ x: ?m.19428x y: ?m.19431y => byGoals accomplished! 🐙 R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: Mx = yrw [R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: Mx = y←one_smul: ∀ (M : Type ?u.19444) {α : Type ?u.19443} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = bone_smul R: Type u_1R x: Mx,R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: M1 • x = y R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: Mx = y←one_smul: ∀ (M : Type ?u.19514) {α : Type ?u.19513} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = bone_smul R: Type u_1R y: My,R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: M1 • x = 1 • y R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: Mx = ySubsingleton.elim: ∀ {α : Sort ?u.19521} [h : Subsingleton α] (a b : α), a = bSubsingleton.elim (1: ?m.195261 : R: Type u_1R) 0: ?m.197110,R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: M0 • x = 0 • y R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: Mx = yzero_smul: ∀ {R : Type ?u.19766} {M : Type ?u.19765} [inst : MonoidWithZero R] [inst_1 : Zero M] [self : MulActionWithZero R M]
(m : M), 0 • m = 0zero_smul,R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: M0 = 0 • y R: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: Mx = yzero_smul: ∀ {R : Type ?u.19902} {M : Type ?u.19901} [inst : MonoidWithZero R] [inst_1 : Zero M] [self : MulActionWithZero R M]
(m : M), 0 • m = 0zero_smulR: Type u_1R': Type ?u.19370M: Type u_2M': Type ?u.19376inst✝⁴: MonoidWithZero Rinst✝³: MonoidWithZero R'inst✝²: Zero Minst✝¹: MulActionWithZero R Minst✝: Subsingleton Rx, y: M0 = 0]Goals accomplished! 🐙⟩
#align mul_action_with_zero.subsingleton MulActionWithZero.subsingleton: ∀ (R : Type u_1) (M : Type u_2) [inst : MonoidWithZero R] [inst_1 : Zero M] [inst : MulActionWithZero R M]
[inst : Subsingleton R], Subsingleton MMulActionWithZero.subsingleton

protected lemma MulActionWithZero.nontrivial: ∀ [inst : MulActionWithZero R M] [inst : Nontrivial M], Nontrivial RMulActionWithZero.nontrivial
[MulActionWithZero: (R : Type ?u.20049) → (M : Type ?u.20048) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.20049?u.20048)MulActionWithZero R: Type ?u.20027R M: Type ?u.20033M] [Nontrivial: Type ?u.20075 → PropNontrivial M: Type ?u.20033M] : Nontrivial: Type ?u.20078 → PropNontrivial R: Type ?u.20027R :=
(subsingleton_or_nontrivial: ∀ (α : Type ?u.20082), Subsingleton α ∨ Nontrivial αsubsingleton_or_nontrivial R: Type ?u.20027R).resolve_left: ∀ {a b : Prop}, a ∨ b → ¬a → bresolve_left fun _: ?m.20092_ =>
not_subsingleton: ∀ (α : Type ?u.20094) [inst : Nontrivial α], ¬Subsingleton αnot_subsingleton M: Type ?u.20033M <| MulActionWithZero.subsingleton: ∀ (R : Type ?u.20101) (M : Type ?u.20102) [inst : MonoidWithZero R] [inst_1 : Zero M] [inst : MulActionWithZero R M]
[inst : Subsingleton R], Subsingleton MMulActionWithZero.subsingleton R: Type ?u.20027R M: Type ?u.20033M
#align mul_action_with_zero.nontrivial MulActionWithZero.nontrivial: ∀ (R : Type u_1) (M : Type u_2) [inst : MonoidWithZero R] [inst_1 : Zero M] [inst : MulActionWithZero R M]
[inst : Nontrivial M], Nontrivial RMulActionWithZero.nontrivial

variable {R: ?m.20169R M: ?m.20172M}
variable [MulActionWithZero: (R : Type ?u.28939) → (M : Type ?u.28938) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.28939?u.28938)MulActionWithZero R: Type ?u.20230R M: Type ?u.20181M] [Zero: Type ?u.20223 → Type ?u.20223Zero M': Type ?u.20239M'] [SMul: Type ?u.20282 → Type ?u.20281 → Type (max?u.20282?u.20281)SMul R: Type ?u.20230R M': Type ?u.24580M']

/-- Pullback a `MulActionWithZero` structure along an injective zero-preserving homomorphism.
See note [reducible non-instances]. -/
@[reducible]
protected def Function.Injective.mulActionWithZero: {R : Type u_1} →
{M : Type u_2} →
{M' : Type u_3} →
[inst : MonoidWithZero R] →
[inst_1 : Zero M] →
[inst_2 : MulActionWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M' M) → Injective ↑f → (∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b) → MulActionWithZero R M'Function.Injective.mulActionWithZero (f: ZeroHom M' Mf : ZeroHom: (M : Type ?u.20286) → (N : Type ?u.20285) → [inst : Zero M] → [inst : Zero N] → Type (max?u.20286?u.20285)ZeroHom M': Type ?u.20239M' M: Type ?u.20236M) (hf: Injective ↑fhf : Function.Injective: {α : Sort ?u.20320} → {β : Sort ?u.20319} → (α → β) → PropFunction.Injective f: ZeroHom M' Mf)
(smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f bsmul : ∀ (a: Ra : R: Type ?u.20230R) (b: ?m.21118b), f: ZeroHom M' Mf (a: Ra • b: ?m.21118b) = a: Ra • f: ZeroHom M' Mf b: ?m.21118b) : MulActionWithZero: (R : Type ?u.22988) → (M : Type ?u.22987) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.22988?u.22987)MulActionWithZero R: Type ?u.20230R M': Type ?u.20239M' :=
{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249{ hf: Injective ↑fhf{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249.mulAction: {M : Type ?u.22999} →
{α : Type ?u.22998} →
{β : Type ?u.22997} →
[inst : Monoid M] →
[inst_1 : MulAction M α] →
[inst_2 : SMul M β] → (f : β → α) → Injective f → (∀ (c : M) (x : β), f (c • x) = c • f x) → MulAction M βmulAction{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249 f: ZeroHom M' Mf{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249 smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f bsmul{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249, hf: Injective ↑fhf{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249.smulWithZero: {R : Type ?u.23983} →
{M : Type ?u.23982} →
{M' : Type ?u.23981} →
[inst : Zero R] →
[inst_1 : Zero M] →
[inst_2 : SMulWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M' M) → Injective ↑f → (∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b) → SMulWithZero R M'smulWithZero{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249 f: ZeroHom M' Mf{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249 smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f bsmul{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249 { hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249with{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249 }
#align function.injective.mul_action_with_zero Function.Injective.mulActionWithZero: {R : Type u_1} →
{M : Type u_2} →
{M' : Type u_3} →
[inst : MonoidWithZero R] →
[inst_1 : Zero M] →
[inst_2 : MulActionWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M' M) →
Function.Injective ↑f → (∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b) → MulActionWithZero R M'Function.Injective.mulActionWithZero

/-- Pushforward a `MulActionWithZero` structure along a surjective zero-preserving homomorphism.
See note [reducible non-instances]. -/
@[reducible]
protected def Function.Surjective.mulActionWithZero: {R : Type u_1} →
{M : Type u_2} →
{M' : Type u_3} →
[inst : MonoidWithZero R] →
[inst_1 : Zero M] →
[inst_2 : MulActionWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M M') → Surjective ↑f → (∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b) → MulActionWithZero R M'Function.Surjective.mulActionWithZero (f: ZeroHom M M'f : ZeroHom: (M : Type ?u.24627) → (N : Type ?u.24626) → [inst : Zero M] → [inst : Zero N] → Type (max?u.24627?u.24626)ZeroHom M: Type ?u.24577M M': Type ?u.24580M') (hf: Surjective ↑fhf : Function.Surjective: {α : Sort ?u.24661} → {β : Sort ?u.24660} → (α → β) → PropFunction.Surjective f: ZeroHom M M'f)
(smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bsmul : ∀ (a: Ra : R: Type ?u.24571R) (b: ?m.25465b), f: ZeroHom M M'f (a: Ra • b: ?m.25465b) = a: Ra • f: ZeroHom M M'f b: ?m.25465b) : MulActionWithZero: (R : Type ?u.27329) → (M : Type ?u.27328) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.27329?u.27328)MulActionWithZero R: Type ?u.24571R M': Type ?u.24580M' :=
{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592{ hf: Surjective ↑fhf{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592.mulAction: {M : Type ?u.27341} →
{α : Type ?u.27340} →
{β : Type ?u.27339} →
[inst : Monoid M] →
[inst_1 : MulAction M α] →
[inst_2 : SMul M β] → (f : α → β) → Surjective f → (∀ (c : M) (x : α), f (c • x) = c • f x) → MulAction M βmulAction{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592 f: ZeroHom M M'f{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592 smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bsmul{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592, hf: Surjective ↑fhf{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592.smulWithZero: {R : Type ?u.28327} →
{M : Type ?u.28326} →
{M' : Type ?u.28325} →
[inst : Zero R] →
[inst_1 : Zero M] →
[inst_2 : SMulWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M M') → Surjective ↑f → (∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b) → SMulWithZero R M'smulWithZero{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592 f: ZeroHom M M'f{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592 smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f bsmul{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592 { hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592with{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592 }
#align function.surjective.mul_action_with_zero Function.Surjective.mulActionWithZero: {R : Type u_1} →
{M : Type u_2} →
{M' : Type u_3} →
[inst : MonoidWithZero R] →
[inst_1 : Zero M] →
[inst_2 : MulActionWithZero R M] →
[inst_3 : Zero M'] →
[inst_4 : SMul R M'] →
(f : ZeroHom M M') →
Function.Surjective ↑f → (∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b) → MulActionWithZero R M'Function.Surjective.mulActionWithZero

variable (M: ?m.28972M)

/-- Compose a `MulActionWithZero` with a `MonoidWithZeroHom`, with action `f r' • m` -/
def MulActionWithZero.compHom: {R : Type u_1} →
{R' : Type u_2} →
(M : Type u_3) →
[inst : MonoidWithZero R] →
[inst_1 : MonoidWithZero R'] →
[inst_2 : Zero M] → [inst_3 : MulActionWithZero R M] → (R' →*₀ R) → MulActionWithZero R' MMulActionWithZero.compHom (f: R' →*₀ Rf : R': Type ?u.28978R' →*₀ R: Type ?u.28975R) : MulActionWithZero: (R : Type ?u.29137) → (M : Type ?u.29136) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.29137?u.29136)MulActionWithZero R': Type ?u.28978R' M: Type ?u.28981M :=
{ SMulWithZero.compHom: {R : Type ?u.29165} →
{R' : Type ?u.29164} →
(M : Type ?u.29163) →
[inst : Zero R] →
[inst_1 : Zero M] → [inst_2 : SMulWithZero R M] → [inst_3 : Zero R'] → ZeroHom R' R → SMulWithZero R' MSMulWithZero.compHom M: Type ?u.28981M f: R' →*₀ Rf.toZeroHom: {M : Type ?u.29246} →
{N : Type ?u.29245} → [inst : MulZeroOneClass M] → [inst_1 : MulZeroOneClass N] → (M →*₀ N) → ZeroHom M NtoZeroHom with
smul := (· • ·): R → M → M(· • ·) ∘ f: R' →*₀ Rf
mul_smul := fun r: ?m.30028r s: ?m.30031s m: ?m.30034m => byGoals accomplished! 🐙 R: Type ?u.28975R': Type ?u.28978M: Type ?u.28981M': Type ?u.28984inst✝⁵: MonoidWithZero Rinst✝⁴: MonoidWithZero R'inst✝³: Zero Minst✝²: MulActionWithZero R Minst✝¹: Zero M'inst✝: SMul R M'f: R' →*₀ Rsrc✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' Mr, s: R'm: M(r * s) • m = r • s • mshow f: R' →*₀ Rf (r: R'r * s: R's) • m: Mm = (f: R' →*₀ Rf r: R'r) • (f: R' →*₀ Rf s: R's) • m: MmR: Type ?u.28975R': Type ?u.28978M: Type ?u.28981M': Type ?u.28984inst✝⁵: MonoidWithZero Rinst✝⁴: MonoidWithZero R'inst✝³: Zero Minst✝²: MulActionWithZero R Minst✝¹: Zero M'inst✝: SMul R M'f: R' →*₀ Rsrc✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' Mr, s: R'm: M↑f (r * s) • m = ↑f r • ↑f s • m;R: Type ?u.28975R': Type ?u.28978M: Type ?u.28981M': Type ?u.28984inst✝⁵: MonoidWithZero Rinst✝⁴: MonoidWithZero R'inst✝³: Zero Minst✝²: MulActionWithZero R Minst✝¹: Zero M'inst✝: SMul R M'f: R' →*₀ Rsrc✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' Mr, s: R'm: M↑f (r * s) • m = ↑f r • ↑f s • m R: Type ?u.28975R': Type ?u.28978M: Type ?u.28981M': Type ?u.28984inst✝⁵: MonoidWithZero Rinst✝⁴: MonoidWithZero R'inst✝³: Zero Minst✝²: MulActionWithZero R Minst✝¹: Zero M'inst✝: SMul R M'f: R' →*₀ Rsrc✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' Mr, s: R'm: M(r * s) • m = r • s • msimp [mul_smul: ∀ {α : Type ?u.34041} {β : Type ?u.34040} [inst : Monoid α] [self : MulAction α β] (x y : α) (b : β),
(x * y) • b = x • y • bmul_smul]Goals accomplished! 🐙
one_smul := fun m: ?m.30018m => byGoals accomplished! 🐙 R: Type ?u.28975R': Type ?u.28978M: Type ?u.28981M': Type ?u.28984inst✝⁵: MonoidWithZero Rinst✝⁴: MonoidWithZero R'inst✝³: Zero Minst✝²: MulActionWithZero R Minst✝¹: Zero M'inst✝: SMul R M'f: R' →*₀ Rsrc✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' Mm: M1 • m = mshow (f: R' →*₀ Rf 1: ?m.308391) • m: Mm = m: MmR: Type ?u.28975R': Type ?u.28978M: Type ?u.28981M': Type ?u.28984inst✝⁵: MonoidWithZero Rinst✝⁴: MonoidWithZero R'inst✝³: Zero Minst✝²: MulActionWithZero R Minst✝¹: Zero M'inst✝: SMul R M'f: R' →*₀ Rsrc✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' Mm: M↑f 1 • m = m;R: Type ?u.28975R': Type ?u.28978M: Type ?u.28981M': Type ?u.28984inst✝⁵: MonoidWithZero Rinst✝⁴: MonoidWithZero R'inst✝³: Zero Minst✝²: MulActionWithZero R Minst✝¹: Zero M'inst✝: SMul R M'f: R' →*₀ Rsrc✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' Mm: M↑f 1 • m = m R: Type ?u.28975R': Type ?u.28978M: Type ?u.28981M': Type ?u.28984inst✝⁵: MonoidWithZero Rinst✝⁴: MonoidWithZero R'inst✝³: Zero Minst✝²: MulActionWithZero R Minst✝¹: Zero M'inst✝: SMul R M'f: R' →*₀ Rsrc✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' Mm: M1 • m = msimpGoals accomplished! 🐙 }
#align mul_action_with_zero.comp_hom MulActionWithZero.compHom: {R : Type u_1} →
{R' : Type u_2} →
(M : Type u_3) →
[inst : MonoidWithZero R] →
[inst_1 : MonoidWithZero R'] →
[inst_2 : Zero M] → [inst_3 : MulActionWithZero R M] → (R' →*₀ R) → MulActionWithZero R' MMulActionWithZero.compHom

end MonoidWithZero

section GroupWithZero

variable {α: Type ?u.35573α β: Type ?u.35576β : Type _: Type (?u.35576+1)Type _} [GroupWithZero: Type ?u.35714 → Type ?u.35714GroupWithZero α: Type ?u.35708α] [GroupWithZero: Type ?u.35717 → Type ?u.35717GroupWithZero β: Type ?u.35576β] [MulActionWithZero: (R : Type ?u.35586) → (M : Type ?u.35585) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.35586?u.35585)MulActionWithZero α: Type ?u.35708α β: Type ?u.35576β]

theorem smul_inv₀: ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : GroupWithZero β] [inst_2 : MulActionWithZero α β]
[inst_3 : SMulCommClass α β β] [inst_4 : IsScalarTower α β β] (c : α) (x : β), (c • x)⁻¹ = c⁻¹ • x⁻¹smul_inv₀ [SMulCommClass: (M : Type ?u.35833) → (N : Type ?u.35832) → (α : Type ?u.35831) → [inst : SMul M α] → [inst : SMul N α] → PropSMulCommClass α: Type ?u.35708α β: Type ?u.35711β β: Type ?u.35711β] [IsScalarTower: (M : Type ?u.36265) →
(N : Type ?u.36264) → (α : Type ?u.36263) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → PropIsScalarTower α: Type ?u.35708α β: Type ?u.35711β β: Type ?u.35711β] (c: αc : α: Type ?u.35708α) (x: βx : β: Type ?u.35711β) :
(c: αc • x: βx)⁻¹ = c: αc⁻¹ • x: βx⁻¹ := byGoals accomplished! 🐙
R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: β(c • x)⁻¹ = c⁻¹ • x⁻¹obtain rfl: c = 0rflrfl | hc: c = 0 ∨ c ≠ 0 | hc: c ≠ 0hc := eq_or_ne: ∀ {α : Sort ?u.37017} (x y : α), x = y ∨ x ≠ yeq_or_ne c: αc 0: ?m.370200R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βx: βinl(0 • x)⁻¹ = 0⁻¹ • x⁻¹R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0inr(c • x)⁻¹ = c⁻¹ • x⁻¹
R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: β(c • x)⁻¹ = c⁻¹ • x⁻¹·R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βx: βinl(0 • x)⁻¹ = 0⁻¹ • x⁻¹ R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βx: βinl(0 • x)⁻¹ = 0⁻¹ • x⁻¹R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0inr(c • x)⁻¹ = c⁻¹ • x⁻¹simp only [inv_zero: ∀ {G₀ : Type ?u.37152} [self : GroupWithZero G₀], 0⁻¹ = 0inv_zero, zero_smul: ∀ (R : Type ?u.37165) {M : Type ?u.37164} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (m : M),
0 • m = 0zero_smul]Goals accomplished! 🐙
R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: β(c • x)⁻¹ = c⁻¹ • x⁻¹obtain rfl: x = 0rflrfl | hx: x = 0 ∨ x ≠ 0 | hx: x ≠ 0hx := eq_or_ne: ∀ {α : Sort ?u.37564} (x y : α), x = y ∨ x ≠ yeq_or_ne x: βx 0: ?m.375670R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αhc: c ≠ 0inr.inl(c • 0)⁻¹ = c⁻¹ • 0⁻¹R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹
R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: β(c • x)⁻¹ = c⁻¹ • x⁻¹·R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αhc: c ≠ 0inr.inl(c • 0)⁻¹ = c⁻¹ • 0⁻¹ R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αhc: c ≠ 0inr.inl(c • 0)⁻¹ = c⁻¹ • 0⁻¹R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹simp only [inv_zero: ∀ {G₀ : Type ?u.37672} [self : GroupWithZero G₀], 0⁻¹ = 0inv_zero, smul_zero: ∀ {M : Type ?u.37679} {A : Type ?u.37678} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0smul_zero]Goals accomplished! 🐙
R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: β(c • x)⁻¹ = c⁻¹ • x⁻¹·R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹ R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹refine' inv_eq_of_mul_eq_one_left: ∀ {α : Type ?u.37815} [inst : DivisionMonoid α] {a b : α}, a * b = 1 → b⁻¹ = ainv_eq_of_mul_eq_one_left _: ?m.37818 * ?m.37819 = 1_R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inrc⁻¹ • x⁻¹ * c • x = 1
R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹rw [R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inrc⁻¹ • x⁻¹ * c • x = 1smul_mul_smul: ∀ {M : Type ?u.37861} {α : Type ?u.37860} [inst : Monoid M] [inst_1 : MulAction M α] [inst_2 : Mul α] (r s : M)
(x y : α) [inst_3 : IsScalarTower M α α] [inst_4 : SMulCommClass M α α], r • x * s • y = (r * s) • (x * y)smul_mul_smul,R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr(c⁻¹ * c) • (x⁻¹ * x) = 1 R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inrc⁻¹ • x⁻¹ * c • x = 1inv_mul_cancel: ∀ {G₀ : Type ?u.38368} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ * a = 1inv_mul_cancel hc: c ≠ 0hc,R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr1 • (x⁻¹ * x) = 1 R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inrc⁻¹ • x⁻¹ * c • x = 1inv_mul_cancel: ∀ {G₀ : Type ?u.38393} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ * a = 1inv_mul_cancel hx: x ≠ 0hx,R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr1 • 1 = 1 R: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inrc⁻¹ • x⁻¹ * c • x = 1one_smul: ∀ (M : Type ?u.38411) {α : Type ?u.38410} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = bone_smulR: Type ?u.35696R': Type ?u.35699M: Type ?u.35702M': Type ?u.35705α: Type u_1β: Type u_2inst✝⁴: GroupWithZero αinst✝³: GroupWithZero βinst✝²: MulActionWithZero α βinst✝¹: SMulCommClass α β βinst✝: IsScalarTower α β βc: αx: βhc: c ≠ 0hx: x ≠ 0inr.inr1 = 1]Goals accomplished! 🐙
#align smul_inv₀ smul_inv₀: ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : GroupWithZero β] [inst_2 : MulActionWithZero α β]
[inst_3 : SMulCommClass α β β] [inst_4 : IsScalarTower α β β] (c : α) (x : β), (c • x)⁻¹ = c⁻¹ • x⁻¹smul_inv₀

end GroupWithZero

/-- Scalar multiplication as a monoid homomorphism with zero. -/
@[simps: ∀ {α : Type u_1} {β : Type u_2} [inst : MonoidWithZero α] [inst_1 : MulZeroOneClass β] [inst_2 : MulActionWithZero α β]
[inst_3 : IsScalarTower α β β] [inst_4 : SMulCommClass α β β] (a : α × β),
↑smulMonoidWithZeroHom a = OneHom.toFun (↑smulMonoidHom) asimps]
def smulMonoidWithZeroHom: {α : Type ?u.38470} →
{β : Type ?u.38473} →
[inst : MonoidWithZero α] →
[inst_1 : MulZeroOneClass β] →
[inst_2 : MulActionWithZero α β] → [inst_3 : IsScalarTower α β β] → [inst_4 : SMulCommClass α β β] → α × β →*₀ βsmulMonoidWithZeroHom {α: Type ?u.38470α β: Type ?u.38473β : Type _: Type (?u.38473+1)Type _} [MonoidWithZero: Type ?u.38476 → Type ?u.38476MonoidWithZero α: Type ?u.38470α] [MulZeroOneClass: Type ?u.38479 → Type ?u.38479MulZeroOneClass β: Type ?u.38473β]
[MulActionWithZero: (R : Type ?u.38483) → (M : Type ?u.38482) → [inst : MonoidWithZero R] → [inst : Zero M] → Type (max?u.38483?u.38482)MulActionWithZero α: Type ?u.38470α β: Type ?u.38473β] [IsScalarTower: (M : Type ?u.38586) →
(N : Type ?u.38585) → (α : Type ?u.38584) → [inst : SMul M N] → [inst : SMul N α] → [inst : SMul M α] → PropIsScalarTower α: Type ?u.38470α β: Type ?u.38473β β: Type ?u.38473β] [SMulCommClass: (M : Type ?u.38974) → (N : Type ?u.38973) → (α : Type ?u.38972) → [inst : SMul M α] → [inst : SMul N α] → PropSMulCommClass α: Type ?u.38470α β: Type ?u.38473β β: Type ?u.38473β] : α: Type ?u.38470α × β: Type ?u.38473β →*₀ β: Type ?u.38473β :=
{ smulMonoidHom: {α : Type ?u.39360} →
{β : Type ?u.39359} →
[inst : Monoid α] →
[inst_1 : MulOneClass β] →
[inst_2 : MulAction α β] → [inst_3 : IsScalarTower α β β] → [inst_4 : SMulCommClass α β β] → α × β →* βsmulMonoidHom with map_zero' := smul_zero: ∀ {M : Type ?u.40677} {A : Type ?u.40676} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0smul_zero _: ?m.40678_ }
#align smul_monoid_with_zero_hom smulMonoidWithZeroHom: {α : Type u_1} →
{β : Type u_2} →
[inst : MonoidWithZero α] →
[inst_1 : MulZeroOneClass β] →
[inst_2 : MulActionWithZero α β] → [inst_3 : IsScalarTower α β β] → [inst_4 : SMulCommClass α β β] → α × β →*₀ βsmulMonoidWithZeroHom
#align smul_monoid_with_zero_hom_apply smulMonoidWithZeroHom_apply: ∀ {α : Type u_1} {β : Type u_2} [inst : MonoidWithZero α] [inst_1 : MulZeroOneClass β] [inst_2 : MulActionWithZero α β]
[inst_3 : IsScalarTower α β β] [inst_4 : SMulCommClass α β β] (a : α × β),
↑smulMonoidWithZeroHom a = OneHom.toFun (↑smulMonoidHom) asmulMonoidWithZeroHom_apply
```