/-
Copyright (c) 2021 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.

We also add an `instance`:

* 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.16491
R R': Type ?u.17
R' M: Type ?u.20
M M': Type ?u.3539
M' : Type _: Type (?u.23+1)
Type _}

section Zero

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

/-- `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.44
Zero R: Type ?u.32
R] [Zero: Type ?u.47 → Type ?u.47
Zero M: Type ?u.38
M] extends SMulZeroClass: Type ?u.53 → (A : Type ?u.52) → [inst : Zero A] → Type (max?u.53?u.52)
SMulZeroClass R: Type ?u.32
R M: Type ?u.38
M 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 = 0
zero_smul : ∀ m: M
m : M: Type ?u.38
M, (0: ?m.88
0 : R: Type ?u.32
R) • m: M
m = 0: ?m.141
0
#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 R
MulZeroClass.toSMulWithZero [MulZeroClass: Type ?u.235 → Type ?u.235
MulZeroClass R: Type ?u.223
R] : 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.223
R R: Type ?u.223
R where
  smul := (· * ·): R → R → R
(· * ·)
  smul_zero := mul_zero: ∀ {M₀ : Type ?u.757} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zero
  zero_smul := zero_mul: ∀ {M₀ : Type ?u.794} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
zero_mul
#align mul_zero_class.to_smul_with_zero MulZeroClass.toSMulWithZero: (R : Type u_1) → [inst : MulZeroClass R] → SMulWithZero R R
MulZeroClass.toSMulWithZero

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

variable {M: ?m.1773
M} [Zero: Type ?u.2224 → Type ?u.2224
Zero R: Type ?u.1761
R] [Zero: Type ?u.3242 → Type ?u.3242
Zero M: Type ?u.3233
M] [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.1761
R M: ?m.1773
M]

@[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 = 0
zero_smul (m: M
m : M: Type ?u.1821
M) : (0: ?m.1880
0 : R: Type ?u.1815
R) • m: M
m = 0: ?m.1988
0 :=
  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 = 0
SMulWithZero.zero_smul m: M
m
#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 = 0
zero_smul

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

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 = 0
smul_eq_zero_of_left (h: a = 0
h : a: R
a = 0: ?m.2270
0) (b: M
b : M: Type ?u.2218
M) : a: R
a • b: M
b = 0: ?m.2405
0 := h: a = 0
h.symm: ∀ {α : Sort ?u.2444} {a b : α}, a = b → b = a
symm ▸ 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 = 0
zero_smul _: Type ?u.2456
_ b: M
b
#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 = 0
smul_eq_zero_of_left
lemma smul_eq_zero_of_right: ∀ (a : R), b = 0 → a • b = 0
smul_eq_zero_of_right (a: R
a : R: Type ?u.2577
R) (h: b = 0
h : b: M
b = 0: ?m.2637
0) : a: R
a • b: M
b = 0: ?m.2770
0 := h: b = 0
h.symm: ∀ {α : Sort ?u.2789} {a b : α}, a = b → b = a
symm ▸ smul_zero: ∀ {M : Type ?u.2801} {A : Type ?u.2800} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero a: R
a
#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 = 0
smul_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 ≠ 0
left_ne_zero_of_smul : a: R
a • b: M
b ≠ 0: ?m.3093
0 → a: R
a ≠ 0: ?m.3119
0 := mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt $ fun h: ?m.3150
h ↦ 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 = 0
smul_eq_zero_of_left h: ?m.3150
h b: M
b
#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 ≠ 0
left_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 ≠ 0
right_ne_zero_of_smul : a: R
a • b: M
b ≠ 0: ?m.3380
0 → b: M
b ≠ 0: ?m.3406
0 := mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt $ 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 = 0
smul_eq_zero_of_right a: R
a
#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 ≠ 0
right_ne_zero_of_smul

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

/-- 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' M
f : 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.3605
M' M: Type ?u.3602
M) (hf: Injective ↑f
hf : Function.Injective: {α : Sort ?u.3697} → {β : Sort ?u.3696} → (α → β) → Prop
Function.Injective f: ZeroHom M' M
f)
    (smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
smul : ∀ (a: R
a : R: Type ?u.3596
R) (b: ?m.4495
b), f: ZeroHom M' M
f (a: R
a • b: ?m.4495
b) = a: R
a • f: ZeroHom M' M
f b: ?m.4495
b) :
    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.3596
R M': Type ?u.3605
M' where
  smul := (· • ·): R → M' → M'
(· • ·)
  zero_smul a: ?m.6399
a := hf: Injective ↑f
hf <| by
Goals accomplished! 🐙 R: Type ?u.3596

R': Type ?u.3599

M: Type ?u.3602

M': Type ?u.3605

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a✝: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M' M

hf: Injective ↑f

smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b

a: M'

↑f (0 • a) = ↑f 0simp [smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
smul]
Goals accomplished! 🐙
  smul_zero a: ?m.6387
a := hf: Injective ↑f
hf <| by
Goals accomplished! 🐙 R: Type ?u.3596

R': Type ?u.3599

M: Type ?u.3602

M': Type ?u.3605

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a✝: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M' M

hf: Injective ↑f

smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b

a: R

↑f (a • 0) = ↑f 0simp [smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
smul]
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.7921
M M': Type ?u.7924
M') (hf: Surjective ↑f
hf : Function.Surjective: {α : Sort ?u.8016} → {β : Sort ?u.8015} → (α → β) → Prop
Function.Surjective f: ZeroHom M M'
f)
    (smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
smul : ∀ (a: R
a : R: Type ?u.7915
R) (b: ?m.8820
b), f: ZeroHom M M'
f (a: R
a • b: ?m.8820
b) = a: R
a • f: ZeroHom M M'
f b: ?m.8820
b) :
    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.7915
R M': Type ?u.7924
M' where
  smul := (· • ·): R → M' → M'
(· • ·)
  zero_smul m: ?m.10719
m := by
Goals accomplished! 🐙
    R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

m: M'

0 • m = 0rcases hf: Surjective ↑f
hf m: M'
m with ⟨x, rfl⟩: ∃ a, ↑f a = m
⟨x: M
x⟨x, rfl⟩: ∃ a, ↑f a = m
, rfl: ↑f x = m
rfl⟨x, rfl⟩: ∃ a, ↑f a = m
⟩R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

x: M

intro0 • ↑f x = 0
    R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

m: M'

0 • m = 0simp [← smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
smul]
Goals accomplished! 🐙
  smul_zero c: ?m.10709
c := by
Goals accomplished! 🐙 R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

c: R

c • 0 = 0rw [R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

c: R

c • 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 = 0
map_zero,R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

c: R

c • ↑f 0 = ↑f 0 R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

c: R

c • 0 = 0←smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
smul,R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

c: R

↑f (c • 0) = ↑f 0 R: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

c: R

c • 0 = 0smul_zero: ∀ {M : Type ?u.10801} {A : Type ?u.10800} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zeroR: Type ?u.7915

R': Type ?u.7918

M: Type ?u.7921

M': Type ?u.7924

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom M M'

hf: Surjective ↑f

smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b

c: 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.11662
M)

/-- 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' M
SMulWithZero.compHom (f: ZeroHom R' R
f : 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.11668
R' R: Type ?u.11665
R) : 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.11668
R' M: Type ?u.11671
M where
  smul := (· • ·): R → M → M
(· • ·) ∘ f: ZeroHom R' R
f
  smul_zero m: ?m.12705
m := smul_zero: ∀ {M : Type ?u.12708} {A : Type ?u.12707} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero (f: ZeroHom R' R
f m: ?m.12705
m)
  zero_smul m: ?m.13667
m := by
Goals accomplished! 🐙 R: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: M

0 • m = 0show (f: ZeroHom R' R
f 0: ?m.14453
0) • m: M
m = 0: ?m.14539
0R: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: M

↑f 0 • m = 0 R: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: M

0 • m = 0;R: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: M

↑f 0 • m = 0 R: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: M

0 • m = 0rw [R: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: 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 = 0
map_zero,R: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: M

0 • m = 0 R: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: 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 = 0
zero_smulR: Type ?u.11665

R': Type ?u.11668

M: Type ?u.11671

M': Type ?u.11674

inst✝⁵: Zero R

inst✝⁴: Zero M

inst✝³: SMulWithZero R M

a: R

b: M

inst✝²: Zero R'

inst✝¹: Zero M'

inst✝: SMul R M'

f: ZeroHom R' R

m: M

0 = 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' M
SMulWithZero.compHom

end Zero

instance AddMonoid.natSMulWithZero: {M : Type u_1} → [inst : AddMonoid M] → SMulWithZero ℕ M
AddMonoid.natSMulWithZero [AddMonoid: Type ?u.15205 → Type ?u.15205
AddMonoid M: Type ?u.15199
M] : 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.15199
M 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 = 0
zero_nsmul
#align add_monoid.nat_smul_with_zero AddMonoid.natSMulWithZero: {M : Type u_1} → [inst : AddMonoid M] → SMulWithZero ℕ M
AddMonoid.natSMulWithZero

instance AddGroup.intSMulWithZero: {M : Type u_1} → [inst : AddGroup M] → SMulWithZero ℤ M
AddGroup.intSMulWithZero [AddGroup: Type ?u.16503 → Type ?u.16503
AddGroup M: Type ?u.16497
M] : 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.16497
M where
  smul_zero := zsmul_zero: ∀ {α : Type ?u.17577} [inst : SubtractionMonoid α] (n : ℤ), n • 0 = 0
zsmul_zero
  zero_smul := zero_zsmul: ∀ {G : Type ?u.17673} [inst : SubNegMonoid G] (a : G), 0 • a = 0
zero_zsmul
#align add_group.int_smul_with_zero AddGroup.intSMulWithZero: {M : Type u_1} → [inst : AddGroup M] → SMulWithZero ℤ M
AddGroup.intSMulWithZero

section MonoidWithZero

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

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

/-- 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.17808
R M: Type ?u.17814
M 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 = 0
smul_zero : ∀ r: R
r : R: Type ?u.17808
R, r: R
r • (0: ?m.17871
0 : M: Type ?u.17814
M) = 0: ?m.17924
0
  /-- 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 = 0
zero_smul : ∀ m: M
m : M: Type ?u.17814
M, (0: ?m.17956
0 : R: Type ?u.17808
R) • m: M
m = 0: ?m.18028
0
#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 M
MulActionWithZero.toSMulWithZero [m: MulActionWithZero R M
m : 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.18102
R M: Type ?u.18108
M] :
    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.18102
R M: Type ?u.18108
M :=
  { m: MulActionWithZero R M
m 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 M
MulActionWithZero.toSMulWithZero

/-- See also `Semiring.toModule` -/
instance MonoidWithZero.toMulActionWithZero: (R : Type u_1) → [inst : MonoidWithZero R] → MulActionWithZero R R
MonoidWithZero.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.18435
R R: Type ?u.18435
R :=
  { MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651
{ MulZeroClass.toSMulWithZero: (R : Type ?u.18514) → [inst : MulZeroClass R] → SMulWithZero R R
MulZeroClass.toSMulWithZero{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651
 R: Type ?u.18435
R{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651
, Monoid.toMulAction: (M : Type ?u.18628) → [inst : Monoid M] → MulAction M M
Monoid.toMulAction{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651
 R: Type ?u.18435
R{ MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651
 { MulZeroClass.toSMulWithZero R, Monoid.toMulAction R with }: MulActionWithZero ?m.18650 ?m.18651
with{ 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 R
MonoidWithZero.toMulActionWithZero

/-- Like `MonoidWithZero.toMulActionWithZero`, but multiplies on the right. See also
`Semiring.toOppositeModule` -/
instance MonoidWithZero.toOppositeMulActionWithZero: MulActionWithZero Rᵐᵒᵖ R
MonoidWithZero.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.18851
Rᵐᵒᵖ R: Type ?u.18851
R :=
  { MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076
{ MulZeroClass.toOppositeSMulWithZero: (R : Type ?u.18939) → [inst : MulZeroClass R] → SMulWithZero Rᵐᵒᵖ R
MulZeroClass.toOppositeSMulWithZero{ MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076
 R: Type ?u.18851
R{ 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.18851
R{ MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076
 { MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }: MulActionWithZero ?m.19075 ?m.19076
with{ 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ᵐᵒᵖ R
MonoidWithZero.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 M
MulActionWithZero.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.19367
R M: Type ?u.19373
M] [Subsingleton: Sort ?u.19415 → Prop
Subsingleton R: Type ?u.19367
R] : Subsingleton: Sort ?u.19418 → Prop
Subsingleton M: Type ?u.19373
M :=
  ⟨λ x: ?m.19428
x y: ?m.19431
y => by
Goals accomplished! 🐙 R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

x = yrw [R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

x = y←one_smul: ∀ (M : Type ?u.19444) {α : Type ?u.19443} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b
one_smul R: Type u_1
R x: M
x,R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

1 • x = y R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

x = y←one_smul: ∀ (M : Type ?u.19514) {α : Type ?u.19513} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b
one_smul R: Type u_1
R y: M
y,R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

1 • x = 1 • y R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

x = ySubsingleton.elim: ∀ {α : Sort ?u.19521} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim (1: ?m.19526
1 : R: Type u_1
R) 0: ?m.19711
0,R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

0 • x = 0 • y R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

x = 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 = 0
zero_smul,R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

0 = 0 • y R: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

x = 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 = 0
zero_smulR: Type u_1

R': Type ?u.19370

M: Type u_2

M': Type ?u.19376

inst✝⁴: MonoidWithZero R

inst✝³: MonoidWithZero R'

inst✝²: Zero M

inst✝¹: MulActionWithZero R M

inst✝: Subsingleton R

x, y: M

0 = 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 M
MulActionWithZero.subsingleton

protected lemma MulActionWithZero.nontrivial: ∀ [inst : MulActionWithZero R M] [inst : Nontrivial M], Nontrivial R
MulActionWithZero.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.20027
R M: Type ?u.20033
M] [Nontrivial: Type ?u.20075 → Prop
Nontrivial M: Type ?u.20033
M] : Nontrivial: Type ?u.20078 → Prop
Nontrivial R: Type ?u.20027
R :=
  (subsingleton_or_nontrivial: ∀ (α : Type ?u.20082), Subsingleton α ∨ Nontrivial α
subsingleton_or_nontrivial R: Type ?u.20027
R).resolve_left: ∀ {a b : Prop}, a ∨ b → ¬a → b
resolve_left fun _: ?m.20092
_ =>
    not_subsingleton: ∀ (α : Type ?u.20094) [inst : Nontrivial α], ¬Subsingleton α
not_subsingleton M: Type ?u.20033
M <| 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 M
MulActionWithZero.subsingleton R: Type ?u.20027
R M: Type ?u.20033
M
#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 R
MulActionWithZero.nontrivial

variable {R: ?m.20169
R M: ?m.20172
M}
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.20230
R M: Type ?u.20181
M] [Zero: Type ?u.20223 → Type ?u.20223
Zero M': Type ?u.20239
M'] [SMul: Type ?u.20282 → Type ?u.20281 → Type (max?u.20282?u.20281)
SMul R: Type ?u.20230
R M': Type ?u.24580
M']

/-- 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' M
f : 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.20239
M' M: Type ?u.20236
M) (hf: Injective ↑f
hf : Function.Injective: {α : Sort ?u.20320} → {β : Sort ?u.20319} → (α → β) → Prop
Function.Injective f: ZeroHom M' M
f)
    (smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
smul : ∀ (a: R
a : R: Type ?u.20230
R) (b: ?m.21118
b), f: ZeroHom M' M
f (a: R
a • b: ?m.21118
b) = a: R
a • f: ZeroHom M' M
f b: ?m.21118
b) : 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.20230
R M': Type ?u.20239
M' :=
  { hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249
{ hf: Injective ↑f
hf{ 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' M
f{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249
 smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
smul{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249
, hf: Injective ↑f
hf{ 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' M
f{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.24248 ?m.24249
 smul: ∀ (a : R) (b : M'), ↑f (a • b) = a • ↑f b
smul{ 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.24249
with{ 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.24577
M M': Type ?u.24580
M') (hf: Surjective ↑f
hf : Function.Surjective: {α : Sort ?u.24661} → {β : Sort ?u.24660} → (α → β) → Prop
Function.Surjective f: ZeroHom M M'
f)
    (smul: ∀ (a : R) (b : M), ↑f (a • b) = a • ↑f b
smul : ∀ (a: R
a : R: Type ?u.24571
R) (b: ?m.25465
b), f: ZeroHom M M'
f (a: R
a • b: ?m.25465
b) = a: R
a • f: ZeroHom M M'
f b: ?m.25465
b) : 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.24571
R M': Type ?u.24580
M' :=
  { hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592
{ hf: Surjective ↑f
hf{ 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 b
smul{ hf.mulAction f smul, hf.smulWithZero f smul with }: MulActionWithZero ?m.28591 ?m.28592
, hf: Surjective ↑f
hf{ 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 b
smul{ 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.28592
with{ 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.28972
M)

/-- 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' M
MulActionWithZero.compHom (f: R' →*₀ R
f : R': Type ?u.28978
R' →*₀ R: Type ?u.28975
R) : 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.28978
R' M: Type ?u.28981
M :=
  { 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' M
SMulWithZero.compHom M: Type ?u.28981
M f: R' →*₀ R
f.toZeroHom: {M : Type ?u.29246} →
  {N : Type ?u.29245} → [inst : MulZeroOneClass M] → [inst_1 : MulZeroOneClass N] → (M →*₀ N) → ZeroHom M N
toZeroHom with
    smul := (· • ·): R → M → M
(· • ·) ∘ f: R' →*₀ R
f
    mul_smul := fun r: ?m.30028
r s: ?m.30031
s m: ?m.30034
m => by
Goals accomplished! 🐙 R: Type ?u.28975

R': Type ?u.28978

M: Type ?u.28981

M': Type ?u.28984

inst✝⁵: MonoidWithZero R

inst✝⁴: MonoidWithZero R'

inst✝³: Zero M

inst✝²: MulActionWithZero R M

inst✝¹: Zero M'

inst✝: SMul R M'

f: R' →*₀ R

src✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' M

r, s: R'

m: M

(r * s) • m = r • s • mshow f: R' →*₀ R
f (r: R'
r * s: R'
s) • m: M
m = (f: R' →*₀ R
f r: R'
r) • (f: R' →*₀ R
f s: R'
s) • m: M
mR: Type ?u.28975

R': Type ?u.28978

M: Type ?u.28981

M': Type ?u.28984

inst✝⁵: MonoidWithZero R

inst✝⁴: MonoidWithZero R'

inst✝³: Zero M

inst✝²: MulActionWithZero R M

inst✝¹: Zero M'

inst✝: SMul R M'

f: R' →*₀ R

src✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' M

r, s: R'

m: M

↑f (r * s) • m = ↑f r • ↑f s • m;R: Type ?u.28975

R': Type ?u.28978

M: Type ?u.28981

M': Type ?u.28984

inst✝⁵: MonoidWithZero R

inst✝⁴: MonoidWithZero R'

inst✝³: Zero M

inst✝²: MulActionWithZero R M

inst✝¹: Zero M'

inst✝: SMul R M'

f: R' →*₀ R

src✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' M

r, s: R'

m: M

↑f (r * s) • m = ↑f r • ↑f s • m R: Type ?u.28975

R': Type ?u.28978

M: Type ?u.28981

M': Type ?u.28984

inst✝⁵: MonoidWithZero R

inst✝⁴: MonoidWithZero R'

inst✝³: Zero M

inst✝²: MulActionWithZero R M

inst✝¹: Zero M'

inst✝: SMul R M'

f: R' →*₀ R

src✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' M

r, 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 • b
mul_smul]
Goals accomplished! 🐙
    one_smul := fun m: ?m.30018
m => by
Goals accomplished! 🐙 R: Type ?u.28975

R': Type ?u.28978

M: Type ?u.28981

M': Type ?u.28984

inst✝⁵: MonoidWithZero R

inst✝⁴: MonoidWithZero R'

inst✝³: Zero M

inst✝²: MulActionWithZero R M

inst✝¹: Zero M'

inst✝: SMul R M'

f: R' →*₀ R

src✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' M

m: M

1 • m = mshow (f: R' →*₀ R
f 1: ?m.30839
1) • m: M
m = m: M
mR: Type ?u.28975

R': Type ?u.28978

M: Type ?u.28981

M': Type ?u.28984

inst✝⁵: MonoidWithZero R

inst✝⁴: MonoidWithZero R'

inst✝³: Zero M

inst✝²: MulActionWithZero R M

inst✝¹: Zero M'

inst✝: SMul R M'

f: R' →*₀ R

src✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' M

m: M

↑f 1 • m = m;R: Type ?u.28975

R': Type ?u.28978

M: Type ?u.28981

M': Type ?u.28984

inst✝⁵: MonoidWithZero R

inst✝⁴: MonoidWithZero R'

inst✝³: Zero M

inst✝²: MulActionWithZero R M

inst✝¹: Zero M'

inst✝: SMul R M'

f: R' →*₀ R

src✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' M

m: M

↑f 1 • m = m R: Type ?u.28975

R': Type ?u.28978

M: Type ?u.28981

M': Type ?u.28984

inst✝⁵: MonoidWithZero R

inst✝⁴: MonoidWithZero R'

inst✝³: Zero M

inst✝²: MulActionWithZero R M

inst✝¹: Zero M'

inst✝: SMul R M'

f: R' →*₀ R

src✝:= SMulWithZero.compHom M ↑f: SMulWithZero R' M

m: M

1 • m = msimp
Goals 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' M
MulActionWithZero.compHom

end MonoidWithZero

section GroupWithZero

variable {α: Type ?u.35573
α β: Type ?u.35576
β : Type _: Type (?u.35576+1)
Type _} [GroupWithZero: Type ?u.35714 → Type ?u.35714
GroupWithZero α: Type ?u.35708
α] [GroupWithZero: Type ?u.35717 → Type ?u.35717
GroupWithZero β: 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 α] → Prop
SMulCommClass α: 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 α] → Prop
IsScalarTower α: 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⁻¹ := by
Goals accomplished! 🐙
  R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

(c • x)⁻¹ = c⁻¹ • x⁻¹obtain rfl: c = 0
rflrfl | hc: c = 0 ∨ c ≠ 0
 | hc: c ≠ 0
hc := eq_or_ne: ∀ {α : Sort ?u.37017} (x y : α), x = y ∨ x ≠ y
eq_or_ne c: α
c 0: ?m.37020
0R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

x: β

inl(0 • x)⁻¹ = 0⁻¹ • x⁻¹
R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

inr(c • x)⁻¹ = c⁻¹ • x⁻¹
  R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

(c • x)⁻¹ = c⁻¹ • x⁻¹·R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

x: β

inl(0 • x)⁻¹ = 0⁻¹ • x⁻¹ R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

x: β

inl(0 • x)⁻¹ = 0⁻¹ • x⁻¹
R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

inr(c • x)⁻¹ = c⁻¹ • x⁻¹simp only [inv_zero: ∀ {G₀ : Type ?u.37152} [self : GroupWithZero G₀], 0⁻¹ = 0
inv_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 = 0
zero_smul]
Goals accomplished! 🐙
  R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

(c • x)⁻¹ = c⁻¹ • x⁻¹obtain rfl: x = 0
rflrfl | hx: x = 0 ∨ x ≠ 0
 | hx: x ≠ 0
hx := eq_or_ne: ∀ {α : Sort ?u.37564} (x y : α), x = y ∨ x ≠ y
eq_or_ne x: β
x 0: ?m.37567
0R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

hc: c ≠ 0

inr.inl(c • 0)⁻¹ = c⁻¹ • 0⁻¹
R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹
  R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

(c • x)⁻¹ = c⁻¹ • x⁻¹·R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

hc: c ≠ 0

inr.inl(c • 0)⁻¹ = c⁻¹ • 0⁻¹ R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

hc: c ≠ 0

inr.inl(c • 0)⁻¹ = c⁻¹ • 0⁻¹
R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹simp only [inv_zero: ∀ {G₀ : Type ?u.37672} [self : GroupWithZero G₀], 0⁻¹ = 0
inv_zero, smul_zero: ∀ {M : Type ?u.37679} {A : Type ?u.37678} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a • 0 = 0
smul_zero]
Goals accomplished! 🐙
  R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

(c • x)⁻¹ = c⁻¹ • x⁻¹·R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹ R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹refine' inv_eq_of_mul_eq_one_left: ∀ {α : Type ?u.37815} [inst : DivisionMonoid α] {a b : α}, a * b = 1 → b⁻¹ = a
inv_eq_of_mul_eq_one_left _: ?m.37818 * ?m.37819 = 1
_R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inrc⁻¹ • x⁻¹ * c • x = 1
    R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inr(c • x)⁻¹ = c⁻¹ • x⁻¹rw [R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.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.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inr(c⁻¹ * c) • (x⁻¹ * x) = 1 R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inrc⁻¹ • x⁻¹ * c • x = 1inv_mul_cancel: ∀ {G₀ : Type ?u.38368} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ * a = 1
inv_mul_cancel hc: c ≠ 0
hc,R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inr1 • (x⁻¹ * x) = 1 R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inrc⁻¹ • x⁻¹ * c • x = 1inv_mul_cancel: ∀ {G₀ : Type ?u.38393} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ * a = 1
inv_mul_cancel hx: x ≠ 0
hx,R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inr1 • 1 = 1 R: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.inrc⁻¹ • x⁻¹ * c • x = 1one_smul: ∀ (M : Type ?u.38411) {α : Type ?u.38410} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b
one_smulR: Type ?u.35696

R': Type ?u.35699

M: Type ?u.35702

M': Type ?u.35705

α: Type u_1

β: Type u_2

inst✝⁴: GroupWithZero α

inst✝³: GroupWithZero β

inst✝²: MulActionWithZero α β

inst✝¹: SMulCommClass α β β

inst✝: IsScalarTower α β β

c: α

x: β

hc: c ≠ 0

hx: x ≠ 0

inr.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) a
simps]
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.38476
MonoidWithZero α: Type ?u.38470
α] [MulZeroOneClass: Type ?u.38479 → Type ?u.38479
MulZeroOneClass β: 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 α] → Prop
IsScalarTower α: 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 α] → Prop
SMulCommClass α: 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 = 0
smul_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) a
smulMonoidWithZeroHom_apply