/-
Copyright (c) 2020 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne Baanen,
  Frédéric Dupuis, Heather Macbeth

! This file was ported from Lean 3 source module algebra.module.linear_map
! leanprover-community/mathlib commit cc8e88c7c8c7bc80f91f84d11adb584bf9bd658f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.GroupAction
import Mathlib.Algebra.Module.Pi
import Mathlib.Algebra.Star.Basic
import Mathlib.Data.Set.Pointwise.SMul
import Mathlib.Algebra.Ring.CompTypeclasses

/-!
# (Semi)linear maps

In this file we define

* `LinearMap σ M M₂`, `M →ₛₗ[σ] M₂` : a semilinear map between two `Module`s. Here,
  `σ` is a `RingHom` from `R` to `R₂` and an `f : M →ₛₗ[σ] M₂` satisfies
  `f (c • x) = (σ c) • (f x)`. We recover plain linear maps by choosing `σ` to be `RingHom.id R`.
  This is denoted by `M →ₗ[R] M₂`. We also add the notation `M →ₗ⋆[R] M₂` for star-linear maps.

* `IsLinearMap R f` : predicate saying that `f : M → M₂` is a linear map. (Note that this
  was not generalized to semilinear maps.)

We then provide `LinearMap` with the following instances:

* `LinearMap.addCommMonoid` and `LinearMap.AddCommGroup`: the elementwise addition structures
  corresponding to addition in the codomain
* `LinearMap.distribMulAction` and `LinearMap.module`: the elementwise scalar action structures
  corresponding to applying the action in the codomain.
* `Module.End.semiring` and `Module.End.ring`: the (semi)ring of endomorphisms formed by taking the
  additive structure above with composition as multiplication.

## Implementation notes

To ensure that composition works smoothly for semilinear maps, we use the typeclasses
`RingHomCompTriple`, `RingHomInvPair` and `RingHomSurjective` from
`Mathlib.Algebra.Ring.CompTypeclasses`.

## Notation

* Throughout the file, we denote regular linear maps by `fₗ`, `gₗ`, etc, and semilinear maps
  by `f`, `g`, etc.

## TODO

* Parts of this file have not yet been generalized to semilinear maps (i.e. `CompatibleSMul`)

## Tags

linear map
-/


assert_not_exists Submonoid
assert_not_exists Finset

open Function

universe u u' v w x y z

variable {R: Type ?u.263916
R : Type _: Type (?u.264788+1)
Type _} {R₁: Type ?u.17
R₁ : Type _: Type (?u.205902+1)
Type _} {R₂: Type ?u.20
R₂ : Type _: Type (?u.266336+1)
Type _} {R₃: Type ?u.23
R₃ : Type _: Type (?u.263925+1)
Type _}
variable {k: Type ?u.26
k : Type _: Type (?u.733631+1)
Type _} {S: Type ?u.263931
S : Type _: Type (?u.708857+1)
Type _} {S₃: Type ?u.266348
S₃ : Type _: Type (?u.251139+1)
Type _} {T: Type ?u.264809
T : Type _: Type (?u.248973+1)
Type _}
variable {M: Type ?u.62
M : Type _: Type (?u.719274+1)
Type _} {M₁: Type ?u.65
M₁ : Type _: Type (?u.263943+1)
Type _} {M₂: Type ?u.266360
M₂ : Type _: Type (?u.526709+1)
Type _} {M₃: Type ?u.107
M₃ : Type _: Type (?u.264821+1)
Type _}
variable {N₁: Type ?u.413026
N₁ : Type _: Type (?u.423584+1)
Type _} {N₂: Type ?u.3585
N₂ : Type _: Type (?u.423587+1)
Type _} {N₃: Type ?u.3588
N₃ : Type _: Type (?u.684264+1)
Type _} {ι: Type ?u.246833
ι : Type _: Type (?u.16195+1)
Type _}

/-- A map `f` between modules over a semiring is linear if it satisfies the two properties
`f (x + y) = f x + f y` and `f (c • x) = c • f x`. The predicate `IsLinearMap R f` asserts this
property. A bundled version is available with `LinearMap`, and should be favored over
`IsLinearMap` most of the time. -/
structure IsLinearMap: (R : Type u) →
  {M : Type v} →
    {M₂ : Type w} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst : Module R M₂] → (M → M₂) → Prop
IsLinearMap (R: Type u
R : Type u: Type (u+1)
Type u) {M: Type v
M : Type v: Type (v+1)
Type v} {M₂: Type w
M₂ : Type w: Type (w+1)
Type w} [Semiring: Type ?u.176 → Type ?u.176
Semiring R: Type u
R] [AddCommMonoid: Type ?u.179 → Type ?u.179
AddCommMonoid M: Type v
M]
  [AddCommMonoid: Type ?u.182 → Type ?u.182
AddCommMonoid M₂: Type w
M₂] [Module: (R : Type ?u.186) → (M : Type ?u.185) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.186?u.185)
Module R: Type u
R M: Type v
M] [Module: (R : Type ?u.212) → (M : Type ?u.211) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.212?u.211)
Module R: Type u
R M₂: Type w
M₂] (f: M → M₂
f : M: Type v
M → M₂: Type w
M₂) : Prop: Type
Prop where
  /-- A linear map preserves addition. -/
  map_add: ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂}, IsLinearMap R f → ∀ (x y : M), f (x + y) = f x + f y
map_add : ∀ x: ?m.241
x y: ?m.244
y, f: M → M₂
f (x: ?m.241
x + y: ?m.244
y) = f: M → M₂
f x: ?m.241
x + f: M → M₂
f y: ?m.244
y
  /-- A linear map preserves scalar multiplication. -/
  map_smul: ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂}, IsLinearMap R f → ∀ (c : R) (x : M), f (c • x) = c • f x
map_smul : ∀ (c: R
c : R: Type u
R) (x: ?m.1916
x), f: M → M₂
f (c: R
c • x: ?m.1916
x) = c: R
c • f: M → M₂
f x: ?m.1916
x
#align is_linear_map IsLinearMap: (R : Type u) →
  {M : Type v} →
    {M₂ : Type w} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst : Module R M₂] → (M → M₂) → Prop
IsLinearMap

section

/-- A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. -/
structure LinearMap: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₂] →
                      (toAddHom : AddHom M M₂) →
                        (∀ (r : R) (x : M), AddHom.toFun toAddHom (r • x) = ↑σ r • AddHom.toFun toAddHom x) →
                          LinearMap σ M M₂
LinearMap {R: Type ?u.3642
R : Type _: Type (?u.3642+1)
Type _} {S: Type ?u.3645
S : Type _: Type (?u.3645+1)
Type _} [Semiring: Type ?u.3648 → Type ?u.3648
Semiring R: Type ?u.3642
R] [Semiring: Type ?u.3651 → Type ?u.3651
Semiring S: Type ?u.3645
S] (σ: R →+* S
σ : R: Type ?u.3642
R →+* S: Type ?u.3645
S) (M: Type ?u.3692
M : Type _: Type (?u.3692+1)
Type _)
    (M₂: Type ?u.3695
M₂ : Type _: Type (?u.3695+1)
Type _) [AddCommMonoid: Type ?u.3698 → Type ?u.3698
AddCommMonoid M: Type ?u.3692
M] [AddCommMonoid: Type ?u.3701 → Type ?u.3701
AddCommMonoid M₂: Type ?u.3695
M₂] [Module: (R : Type ?u.3705) → (M : Type ?u.3704) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.3705?u.3704)
Module R: Type ?u.3642
R M: Type ?u.3692
M] [Module: (R : Type ?u.3729) → (M : Type ?u.3728) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.3729?u.3728)
Module S: Type ?u.3645
S M₂: Type ?u.3695
M₂] extends
    AddHom: (M : Type ?u.3755) → (N : Type ?u.3754) → [inst : Add M] → [inst : Add N] → Type (max?u.3755?u.3754)
AddHom M: Type ?u.3692
M M₂: Type ?u.3695
M₂ where
  /-- A linear map preserves scalar multiplication.
  We prefer the spelling `_root_.map_smul` instead. -/
  map_smul': ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_3} {M₂ : Type u_4}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  (self : LinearMap σ M M₂) (r : R) (x : M), AddHom.toFun self.toAddHom (r • x) = ↑σ r • AddHom.toFun self.toAddHom x
map_smul' : ∀ (r: R
r : R: Type ?u.3642
R) (x: M
x : M: Type ?u.3692
M), toFun: M → M₂
toFun (r: R
r • x: M
x) = σ: R →+* S
σ r: R
r • toFun: M → M₂
toFun x: M
x
#align linear_map LinearMap: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (R →+* S) →
          (M : Type u_3) →
            (M₂ : Type u_4) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (maxu_3u_4)
LinearMap

/-- The `AddHom` underlying a `LinearMap`. -/
add_decl_doc LinearMap.toAddHom: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] → [inst_5 : Module S M₂] → LinearMap σ M M₂ → AddHom M M₂
LinearMap.toAddHom
#align linear_map.to_add_hom LinearMap.toAddHom: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] → [inst_5 : Module S M₂] → LinearMap σ M M₂ → AddHom M M₂
LinearMap.toAddHom

-- mathport name: «expr →ₛₗ[ ] »
/-- `M →ₛₗ[σ] N` is the type of `σ`-semilinear maps from `M` to `N`. -/
notation:25 M: ?m.10079
M " →ₛₗ[" σ: ?m.10086
σ:25 "] " M₂: ?m.10070
M₂:0 => LinearMap: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (R →+* S) →
          (M : Type u_3) →
            (M₂ : Type u_4) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (maxu_3u_4)
LinearMap σ: ?m.10828
σ M: ?m.10821
M M₂: ?m.10070
M₂

/-- `M →ₗ[R] N` is the type of `R`-linear maps from `M` to `N`. -/
-- mathport name: «expr →ₗ[ ] »
notation:25 M: ?m.18954
M " →ₗ[" R: ?m.18961
R:25 "] " M₂: ?m.16408
M₂:0 => LinearMap: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (R →+* S) →
          (M : Type u_3) →
            (M₂ : Type u_4) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (maxu_3u_4)
LinearMap (RingHom.id: (α : Type u_1) → [inst : NonAssocSemiring α] → α →+* α
RingHom.id R: ?m.16417
R) M: ?m.20126
M M₂: ?m.20803
M₂

/-- `M →ₗ⋆[R] N` is the type of `R`-conjugate-linear maps from `M` to `N`. -/
-- mathport name: «expr →ₗ⋆[ ] »
notation:25 M: ?m.34342
M " →ₗ⋆[" R: ?m.34349
R:25 "] " M₂: ?m.34333
M₂:0 => LinearMap: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (R →+* S) →
          (M : Type u_3) →
            (M₂ : Type u_4) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (maxu_3u_4)
LinearMap (starRingEnd: (R : Type u) → [inst : CommSemiring R] → [inst_1 : StarRing R] → R →+* R
starRingEnd R: ?m.31843
R) M: ?m.36198
M M₂: ?m.36191
M₂

/-- `SemilinearMapClass F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear maps `M → M₂`.

See also `LinearMapClass F R M M₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. -/
class SemilinearMapClass: {F : Type u_1} →
  {R : outParam (Type u_2)} →
    {S : outParam (Type u_3)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          {σ : outParam (R →+* S)} →
            {M : outParam (Type u_4)} →
              {M₂ : outParam (Type u_5)} →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : Module R M] →
                      [inst_5 : Module S M₂] →
                        [toAddHomClass : AddHomClass F M M₂] →
                          (∀ (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x) → SemilinearMapClass F σ M M₂
SemilinearMapClass (F: Type ?u.46983
F : Type _: Type (?u.46983+1)
Type _) {R: outParam (Type ?u.46987)
R S: outParam (Type ?u.46991)
S : outParam: Sort ?u.46986 → Sort ?u.46986
outParam (Type _: Type (?u.46987+1)
Type _)} [Semiring: Type ?u.46994 → Type ?u.46994
Semiring R: outParam (Type ?u.46987)
R] [Semiring: Type ?u.46997 → Type ?u.46997
Semiring S: outParam (Type ?u.46991)
S]
  (σ: outParam (R →+* S)
σ : outParam: Sort ?u.47000 → Sort ?u.47000
outParam (R: outParam (Type ?u.46987)
R →+* S: outParam (Type ?u.46991)
S)) (M: outParam (Type ?u.47040)
M M₂: outParam (Type ?u.47044)
M₂ : outParam: Sort ?u.47039 → Sort ?u.47039
outParam (Type _: Type (?u.47040+1)
Type _)) [AddCommMonoid: Type ?u.47047 → Type ?u.47047
AddCommMonoid M: outParam (Type ?u.47040)
M] [AddCommMonoid: Type ?u.47050 → Type ?u.47050
AddCommMonoid M₂: outParam (Type ?u.47044)
M₂]
  [Module: (R : Type ?u.47054) →
  (M : Type ?u.47053) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.47054?u.47053)
Module R: outParam (Type ?u.46987)
R M: outParam (Type ?u.47040)
M] [Module: (R : Type ?u.47078) →
  (M : Type ?u.47077) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.47078?u.47077)
Module S: outParam (Type ?u.46991)
S M₂: outParam (Type ?u.47044)
M₂] extends AddHomClass: Type ?u.47105 →
  (M : outParam (Type ?u.47104)) →
    (N : outParam (Type ?u.47103)) → [inst : Add M] → [inst : Add N] → Type (max(max?u.47105?u.47104)?u.47103)
AddHomClass F: Type ?u.46983
F M: outParam (Type ?u.47040)
M M₂: outParam (Type ?u.47044)
M₂ where
  /-- A semilinear map preserves scalar multiplication up to some ring homomorphism `σ`.
  See also `_root_.map_smul` for the case where `σ` is the identity. -/
  map_smulₛₗ: ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : outParam (R →+* S)} {M : outParam (Type u_4)} {M₂ : outParam (Type u_5)} [inst_2 : AddCommMonoid M]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] [self : SemilinearMapClass F σ M M₂] (f : F)
  (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x
map_smulₛₗ : ∀ (f: F
f : F: Type ?u.46983
F) (r: R
r : R: outParam (Type ?u.46987)
R) (x: M
x : M: outParam (Type ?u.47040)
M), f: F
f (r: R
r • x: M
x) = σ: outParam (R →+* S)
σ r: R
r • f: F
f x: M
x
#align semilinear_map_class SemilinearMapClass: Type u_1 →
  {R : outParam (Type u_2)} →
    {S : outParam (Type u_3)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type u_4)) →
              (M₂ : outParam (Type u_5)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst : Module R M] → [inst : Module S M₂] → Type (max(maxu_1u_4)u_5)
SemilinearMapClass

end

-- Porting note: `dangerousInstance` linter has become smarter about `outParam`s
-- `σ` becomes a metavariable but that's fine because it's an `outParam`
-- attribute [nolint dangerousInstance] SemilinearMapClass.toAddHomClass

export SemilinearMapClass (map_smulₛₗ)

attribute [simp] map_smulₛₗ: ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : outParam (R →+* S)} {M : outParam (Type u_4)} {M₂ : outParam (Type u_5)} [inst_2 : AddCommMonoid M]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] [self : SemilinearMapClass F σ M M₂] (f : F)
  (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x
map_smulₛₗ

/-- `LinearMapClass F R M M₂` asserts `F` is a type of bundled `R`-linear maps `M → M₂`.

This is an abbreviation for `SemilinearMapClass F (RingHom.id R) M M₂`.
-/
abbrev LinearMapClass: (F : Type ?u.50736) →
  (R : outParam (Type ?u.50740)) →
    (M : outParam (Type ?u.50744)) →
      (M₂ : outParam (Type ?u.50748)) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → ?m.50811 F R M M₂
LinearMapClass (F: Type ?u.50736
F : Type _: Type (?u.50736+1)
Type _) (R: outParam (Type ?u.50740)
R M: outParam (Type ?u.50744)
M M₂: outParam (Type ?u.50748)
M₂ : outParam: Sort ?u.50747 → Sort ?u.50747
outParam (Type _: Type (?u.50748+1)
Type _)) [Semiring: Type ?u.50751 → Type ?u.50751
Semiring R: outParam (Type ?u.50740)
R] [AddCommMonoid: Type ?u.50754 → Type ?u.50754
AddCommMonoid M: outParam (Type ?u.50744)
M]
    [AddCommMonoid: Type ?u.50757 → Type ?u.50757
AddCommMonoid M₂: outParam (Type ?u.50748)
M₂] [Module: (R : Type ?u.50761) →
  (M : Type ?u.50760) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.50761?u.50760)
Module R: outParam (Type ?u.50740)
R M: outParam (Type ?u.50744)
M] [Module: (R : Type ?u.50787) →
  (M : Type ?u.50786) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.50787?u.50786)
Module R: outParam (Type ?u.50740)
R M₂: outParam (Type ?u.50748)
M₂] :=
  SemilinearMapClass: Type ?u.50826 →
  {R : outParam (Type ?u.50825)} →
    {S : outParam (Type ?u.50824)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type ?u.50823)) →
              (M₂ : outParam (Type ?u.50822)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst : Module R M] → [inst : Module S M₂] → Type (max(max?u.50826?u.50823)?u.50822)
SemilinearMapClass F: Type ?u.50736
F (RingHom.id: (α : Type ?u.50860) → [inst : NonAssocSemiring α] → α →+* α
RingHom.id R: outParam (Type ?u.50740)
R) M: outParam (Type ?u.50744)
M M₂: outParam (Type ?u.50748)
M₂
#align linear_map_class LinearMapClass: Type u_1 →
  (R : outParam (Type u_2)) →
    (M : outParam (Type u_3)) →
      (M₂ : outParam (Type u_4)) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst : Module R M₂] → Type (max(maxu_1u_3)u_4)
LinearMapClass

namespace SemilinearMapClass

variable (F: Type ?u.51588
F : Type _: Type (?u.51168+1)
Type _)
variable [Semiring: Type ?u.51249 → Type ?u.51249
Semiring R: Type ?u.50994
R] [Semiring: Type ?u.51252 → Type ?u.51252
Semiring S: Type ?u.51009
S]
variable [AddCommMonoid: Type ?u.51255 → Type ?u.51255
AddCommMonoid M: Type ?u.51376
M] [AddCommMonoid: Type ?u.51180 → Type ?u.51180
AddCommMonoid M₁: Type ?u.51078
M₁] [AddCommMonoid: Type ?u.51415 → Type ?u.51415
AddCommMonoid M₂: Type ?u.51081
M₂] [AddCommMonoid: Type ?u.51418 → Type ?u.51418
AddCommMonoid M₃: Type ?u.72086
M₃]
variable [AddCommMonoid: Type ?u.51609 → Type ?u.51609
AddCommMonoid N₁: Type ?u.51156
N₁] [AddCommMonoid: Type ?u.51612 → Type ?u.51612
AddCommMonoid N₂: Type ?u.51159
N₂] [AddCommMonoid: Type ?u.51195 → Type ?u.51195
AddCommMonoid N₃: Type ?u.51162
N₃]
variable [Module: (R : Type ?u.64878) →
  (M : Type ?u.64877) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.64878?u.64877)
Module R: Type ?u.51352
R M: Type ?u.51376
M] [Module: (R : Type ?u.64904) →
  (M : Type ?u.64903) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.64904?u.64903)
Module R: Type ?u.51352
R M₂: Type ?u.51382
M₂] [Module: (R : Type ?u.51327) →
  (M : Type ?u.51326) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.51327?u.51326)
Module S: Type ?u.51213
S M₃: Type ?u.51231
M₃]
variable {σ: R →+* S
σ : R: Type ?u.51540
R →+* S: Type ?u.51367
S}

-- Porting note: the `dangerousInstance` linter has become smarter about `outParam`s
instance (priority := 100) addMonoidHomClass: {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {M₃ : Type u_4} →
        (F : Type u_5) →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₃] →
                      {σ : R →+* S} → [inst : SemilinearMapClass F σ M M₃] → AddMonoidHomClass F M M₃
addMonoidHomClass [SemilinearMapClass: Type ?u.51732 →
  {R : outParam (Type ?u.51731)} →
    {S : outParam (Type ?u.51730)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type ?u.51729)) →
              (M₂ : outParam (Type ?u.51728)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst : Module R M] → [inst : Module S M₂] → Type (max(max?u.51732?u.51729)?u.51728)
SemilinearMapClass F: Type ?u.51588
F σ: R →+* S
σ M: Type ?u.51564
M M₃: Type ?u.51573
M₃] :
    AddMonoidHomClass: Type ?u.51817 →
  (M : outParam (Type ?u.51816)) →
    (N : outParam (Type ?u.51815)) →
      [inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.51817?u.51816)?u.51815)
AddMonoidHomClass F: Type ?u.51588
F M: Type ?u.51564
M M₃: Type ?u.51573
M₃ :=
  { SemilinearMapClass.toAddHomClass: {F : Type ?u.52642} →
  {R : outParam (Type ?u.52641)} →
    {S : outParam (Type ?u.52640)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          {σ : outParam (R →+* S)} →
            {M : outParam (Type ?u.52639)} →
              {M₂ : outParam (Type ?u.52638)} →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : Module R M] →
                      [inst_5 : Module S M₂] → [self : SemilinearMapClass F σ M M₂] → AddHomClass F M M₂
SemilinearMapClass.toAddHomClass with
    coe := fun f: ?m.54293
f ↦ (f: ?m.54293
f : M: Type ?u.51564
M → M₃: Type ?u.51573
M₃)
    map_zero := fun f: ?m.57005
f ↦
      show f: ?m.57005
f 0: ?m.58089
0 = 0: ?m.58575
0 by
        rw [R: Type ?u.51540

R₁: Type ?u.51543

R₂: Type ?u.51546

R₃: Type ?u.51549

k: Type ?u.51552

S: Type ?u.51555

S₃: Type ?u.51558

T: Type ?u.51561

M: Type ?u.51564

M₁: Type ?u.51567

M₂: Type ?u.51570

M₃: Type ?u.51573

N₁: Type ?u.51576

N₂: Type ?u.51579

N₃: Type ?u.51582

ι: Type ?u.51585

F: Type ?u.51588

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: SemilinearMapClass F σ M M₃

src✝:= toAddHomClass: AddHomClass F M M₃

f: F

↑f 0 = 0← zero_smul: ∀ (R : Type ?u.60550) {M : Type ?u.60549} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (m : M),
  0 • m = 0
zero_smul R: Type ?u.51540
R (0: ?m.60557
0 : M: Type ?u.51564
M),R: Type ?u.51540

R₁: Type ?u.51543

R₂: Type ?u.51546

R₃: Type ?u.51549

k: Type ?u.51552

S: Type ?u.51555

S₃: Type ?u.51558

T: Type ?u.51561

M: Type ?u.51564

M₁: Type ?u.51567

M₂: Type ?u.51570

M₃: Type ?u.51573

N₁: Type ?u.51576

N₂: Type ?u.51579

N₃: Type ?u.51582

ι: Type ?u.51585

F: Type ?u.51588

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: SemilinearMapClass F σ M M₃

src✝:= toAddHomClass: AddHomClass F M M₃

f: F

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

R₁: Type ?u.51543

R₂: Type ?u.51546

R₃: Type ?u.51549

k: Type ?u.51552

S: Type ?u.51555

S₃: Type ?u.51558

T: Type ?u.51561

M: Type ?u.51564

M₁: Type ?u.51567

M₂: Type ?u.51570

M₃: Type ?u.51573

N₁: Type ?u.51576

N₂: Type ?u.51579

N₃: Type ?u.51582

ι: Type ?u.51585

F: Type ?u.51588

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: SemilinearMapClass F σ M M₃

src✝:= toAddHomClass: AddHomClass F M M₃

f: F

↑f 0 = 0map_smulₛₗ: ∀ {F : Type ?u.61264} {R : outParam (Type ?u.61263)} {S : outParam (Type ?u.61262)} [inst : Semiring R]
  [inst_1 : Semiring S] {σ : outParam (R →+* S)} {M : outParam (Type ?u.61261)} {M₂ : outParam (Type ?u.61260)}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  [self : SemilinearMapClass F σ M M₂] (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x
map_smulₛₗR: Type ?u.51540

R₁: Type ?u.51543

R₂: Type ?u.51546

R₃: Type ?u.51549

k: Type ?u.51552

S: Type ?u.51555

S₃: Type ?u.51558

T: Type ?u.51561

M: Type ?u.51564

M₁: Type ?u.51567

M₂: Type ?u.51570

M₃: Type ?u.51573

N₁: Type ?u.51576

N₂: Type ?u.51579

N₃: Type ?u.51582

ι: Type ?u.51585

F: Type ?u.51588

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: SemilinearMapClass F σ M M₃

src✝:= toAddHomClass: AddHomClass F M M₃

f: F

↑σ 0 • ↑f 0 = 0]R: Type ?u.51540

R₁: Type ?u.51543

R₂: Type ?u.51546

R₃: Type ?u.51549

k: Type ?u.51552

S: Type ?u.51555

S₃: Type ?u.51558

T: Type ?u.51561

M: Type ?u.51564

M₁: Type ?u.51567

M₂: Type ?u.51570

M₃: Type ?u.51573

N₁: Type ?u.51576

N₂: Type ?u.51579

N₃: Type ?u.51582

ι: Type ?u.51585

F: Type ?u.51588

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: SemilinearMapClass F σ M M₃

src✝:= toAddHomClass: AddHomClass F M M₃

f: F

↑σ 0 • ↑f 0 = 0
        R: Type ?u.51540

R₁: Type ?u.51543

R₂: Type ?u.51546

R₃: Type ?u.51549

k: Type ?u.51552

S: Type ?u.51555

S₃: Type ?u.51558

T: Type ?u.51561

M: Type ?u.51564

M₁: Type ?u.51567

M₂: Type ?u.51570

M₃: Type ?u.51573

N₁: Type ?u.51576

N₂: Type ?u.51579

N₃: Type ?u.51582

ι: Type ?u.51585

F: Type ?u.51588

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: SemilinearMapClass F σ M M₃

src✝:= toAddHomClass: AddHomClass F M M₃

f: F

↑f 0 = 0simp
Goals accomplished! 🐙 }

instance (priority := 100) distribMulActionHomClass: {R : Type u_1} →
  {M : Type u_2} →
    {M₂ : Type u_3} →
      (F : Type u_4) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M₂] → [inst_5 : LinearMapClass F R M M₂] → DistribMulActionHomClass F R M M₂
distribMulActionHomClass [LinearMapClass: Type ?u.64990 →
  (R : outParam (Type ?u.64989)) →
    (M : outParam (Type ?u.64988)) →
      (M₂ : outParam (Type ?u.64987)) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : Module R M] → [inst : Module R M₂] → Type (max(max?u.64990?u.64988)?u.64987)
LinearMapClass F: Type ?u.64847
F R: Type ?u.64799
R M: Type ?u.64823
M M₂: Type ?u.64829
M₂] :
    DistribMulActionHomClass: Type ?u.65052 →
  (M : outParam (Type ?u.65051)) →
    (A : outParam (Type ?u.65050)) →
      (B : outParam (Type ?u.65049)) →
        [inst : Monoid M] →
          [inst_1 : AddMonoid A] →
            [inst_2 : AddMonoid B] →
              [inst_3 : DistribMulAction M A] →
                [inst : DistribMulAction M B] → Type (max(max?u.65052?u.65050)?u.65049)
DistribMulActionHomClass F: Type ?u.64847
F R: Type ?u.64799
R M: Type ?u.64823
M M₂: Type ?u.64829
M₂ :=
  { SemilinearMapClass.addMonoidHomClass: {R : Type ?u.65967} →
  {S : Type ?u.65966} →
    {M : Type ?u.65965} →
      {M₃ : Type ?u.65964} →
        (F : Type ?u.65963) →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₃] →
                      {σ : R →+* S} → [inst : SemilinearMapClass F σ M M₃] → AddMonoidHomClass F M M₃
SemilinearMapClass.addMonoidHomClass F: Type ?u.64847
F with
    coe := fun f: ?m.68292
f ↦ (f: ?m.68292
f : M: Type ?u.64823
M → M₂: Type ?u.64829
M₂)
    map_smul := fun f: ?m.70805
f c: ?m.70808
c x: ?m.70811
x ↦ by
Goals accomplished! 🐙 R: Type ?u.64799

R₁: Type ?u.64802

R₂: Type ?u.64805

R₃: Type ?u.64808

k: Type ?u.64811

S: Type ?u.64814

S₃: Type ?u.64817

T: Type ?u.64820

M: Type ?u.64823

M₁: Type ?u.64826

M₂: Type ?u.64829

M₃: Type ?u.64832

N₁: Type ?u.64835

N₂: Type ?u.64838

N₃: Type ?u.64841

ι: Type ?u.64844

F: Type ?u.64847

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: LinearMapClass F R M M₂

src✝:= addMonoidHomClass F: AddMonoidHomClass F M M₂

f: F

c: R

x: M

↑f (c • x) = c • ↑f xrw [R: Type ?u.64799

R₁: Type ?u.64802

R₂: Type ?u.64805

R₃: Type ?u.64808

k: Type ?u.64811

S: Type ?u.64814

S₃: Type ?u.64817

T: Type ?u.64820

M: Type ?u.64823

M₁: Type ?u.64826

M₂: Type ?u.64829

M₃: Type ?u.64832

N₁: Type ?u.64835

N₂: Type ?u.64838

N₃: Type ?u.64841

ι: Type ?u.64844

F: Type ?u.64847

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: LinearMapClass F R M M₂

src✝:= addMonoidHomClass F: AddMonoidHomClass F M M₂

f: F

c: R

x: M

↑f (c • x) = c • ↑f xmap_smulₛₗ: ∀ {F : Type ?u.70902} {R : outParam (Type ?u.70901)} {S : outParam (Type ?u.70900)} [inst : Semiring R]
  [inst_1 : Semiring S] {σ : outParam (R →+* S)} {M : outParam (Type ?u.70899)} {M₂ : outParam (Type ?u.70898)}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  [self : SemilinearMapClass F σ M M₂] (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x
map_smulₛₗ,R: Type ?u.64799

R₁: Type ?u.64802

R₂: Type ?u.64805

R₃: Type ?u.64808

k: Type ?u.64811

S: Type ?u.64814

S₃: Type ?u.64817

T: Type ?u.64820

M: Type ?u.64823

M₁: Type ?u.64826

M₂: Type ?u.64829

M₃: Type ?u.64832

N₁: Type ?u.64835

N₂: Type ?u.64838

N₃: Type ?u.64841

ι: Type ?u.64844

F: Type ?u.64847

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: LinearMapClass F R M M₂

src✝:= addMonoidHomClass F: AddMonoidHomClass F M M₂

f: F

c: R

x: M

↑(RingHom.id R) c • ↑f x = c • ↑f x R: Type ?u.64799

R₁: Type ?u.64802

R₂: Type ?u.64805

R₃: Type ?u.64808

k: Type ?u.64811

S: Type ?u.64814

S₃: Type ?u.64817

T: Type ?u.64820

M: Type ?u.64823

M₁: Type ?u.64826

M₂: Type ?u.64829

M₃: Type ?u.64832

N₁: Type ?u.64835

N₂: Type ?u.64838

N₃: Type ?u.64841

ι: Type ?u.64844

F: Type ?u.64847

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: LinearMapClass F R M M₂

src✝:= addMonoidHomClass F: AddMonoidHomClass F M M₂

f: F

c: R

x: M

↑f (c • x) = c • ↑f xRingHom.id_apply: ∀ {α : Type ?u.71354} {x : NonAssocSemiring α} (x_1 : α), ↑(RingHom.id α) x_1 = x_1
RingHom.id_applyR: Type ?u.64799

R₁: Type ?u.64802

R₂: Type ?u.64805

R₃: Type ?u.64808

k: Type ?u.64811

S: Type ?u.64814

S₃: Type ?u.64817

T: Type ?u.64820

M: Type ?u.64823

M₁: Type ?u.64826

M₂: Type ?u.64829

M₃: Type ?u.64832

N₁: Type ?u.64835

N₂: Type ?u.64838

N₃: Type ?u.64841

ι: Type ?u.64844

F: Type ?u.64847

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

inst✝: LinearMapClass F R M M₂

src✝:= addMonoidHomClass F: AddMonoidHomClass F M M₂

f: F

c: R

x: M

c • ↑f x = c • ↑f x]
Goals accomplished! 🐙 }

variable {F: ?m.71969
F} (f: F
f : F: ?m.71969
F) [i: SemilinearMapClass F σ M M₃
i : SemilinearMapClass: Type ?u.72247 →
  {R : outParam (Type ?u.72246)} →
    {S : outParam (Type ?u.72245)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type ?u.72244)) →
              (M₂ : outParam (Type ?u.72243)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst : Module R M] → [inst : Module S M₂] → Type (max(max?u.72247?u.72244)?u.72243)
SemilinearMapClass F: ?m.71969
F σ: R →+* S
σ M: Type ?u.71805
M M₃: Type ?u.71814
M₃]

theorem map_smul_inv: ∀ {R : Type u_2} {S : Type u_1} {M : Type u_5} {M₃ : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : F) [i : SemilinearMapClass F σ M M₃] {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] (c : S) (x : M),
  c • ↑f x = ↑f (↑σ' c • x)
map_smul_inv {σ': S →+* R
σ' : S: Type ?u.72068
S →+* R: Type ?u.72053
R} [RingHomInvPair: {R₁ : Type ?u.72361} →
  {R₂ : Type ?u.72360} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → (R₁ →+* R₂) → outParam (R₂ →+* R₁) → Prop
RingHomInvPair σ: R →+* S
σ σ': S →+* R
σ'] (c: S
c : S: Type ?u.72068
S) (x: M
x : M: Type ?u.72077
M) :
    c: S
c • f: F
f x: M
x = f: F
f (σ': S →+* R
σ' c: S
c • x: M
x) := by
Goals accomplished! 🐙 R: Type u_2

R₁: Type ?u.72056

R₂: Type ?u.72059

R₃: Type ?u.72062

k: Type ?u.72065

S: Type u_1

S₃: Type ?u.72071

T: Type ?u.72074

M: Type u_5

M₁: Type ?u.72080

M₂: Type ?u.72083

M₃: Type u_3

N₁: Type ?u.72089

N₂: Type ?u.72092

N₃: Type ?u.72095

ι: Type ?u.72098

F: Type u_4

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

f: F

i: SemilinearMapClass F σ M M₃

σ': S →+* R

inst✝: RingHomInvPair σ σ'

c: S

x: M

c • ↑f x = ↑f (↑σ' c • x)simp
Goals accomplished! 🐙
#align semilinear_map_class.map_smul_inv SemilinearMapClass.map_smul_inv: ∀ {R : Type u_2} {S : Type u_1} {M : Type u_5} {M₃ : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : F) [i : SemilinearMapClass F σ M M₃] {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] (c : S) (x : M),
  c • ↑f x = ↑f (↑σ' c • x)
SemilinearMapClass.map_smul_inv

end SemilinearMapClass

namespace LinearMap

section AddCommMonoid

variable [Semiring: Type ?u.129675 → Type ?u.129675
Semiring R: Type ?u.116234
R] [Semiring: Type ?u.115372 → Type ?u.115372
Semiring S: Type ?u.79682
S]

section

variable [AddCommMonoid: Type ?u.83959 → Type ?u.83959
AddCommMonoid M: Type ?u.79745
M] [AddCommMonoid: Type ?u.83962 → Type ?u.83962
AddCommMonoid M₁: Type ?u.79748
M₁] [AddCommMonoid: Type ?u.104524 → Type ?u.104524
AddCommMonoid M₂: Type ?u.79817
M₂] [AddCommMonoid: Type ?u.108446 → Type ?u.108446
AddCommMonoid M₃: Type ?u.79754
M₃]

variable [AddCommMonoid: Type ?u.99041 → Type ?u.99041
AddCommMonoid N₁: Type ?u.79898
N₁] [AddCommMonoid: Type ?u.95823 → Type ?u.95823
AddCommMonoid N₂: Type ?u.96539
N₂] [AddCommMonoid: Type ?u.98378 → Type ?u.98378
AddCommMonoid N₃: Type ?u.79829
N₃]

variable [Module: (R : Type ?u.92262) →
  (M : Type ?u.92261) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.92262?u.92261)
Module R: Type ?u.79862
R M: Type ?u.98999
M] [Module: (R : Type ?u.79964) →
  (M : Type ?u.79963) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.79964?u.79963)
Module R: Type ?u.79862
R M₂: Type ?u.79892
M₂] [Module: (R : Type ?u.80139) →
  (M : Type ?u.80138) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.80139?u.80138)
Module S: Type ?u.79877
S M₃: Type ?u.79895
M₃]

variable {σ: R →+* S
σ : R: Type ?u.80013
R →+* S: Type ?u.80028
S}

instance semilinearMapClass: SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
semilinearMapClass : SemilinearMapClass: Type ?u.80387 →
  {R : outParam (Type ?u.80386)} →
    {S : outParam (Type ?u.80385)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type ?u.80384)) →
              (M₂ : outParam (Type ?u.80383)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst : Module R M] → [inst : Module S M₂] → Type (max(max?u.80387?u.80384)?u.80383)
SemilinearMapClass (M: Type ?u.80222
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.80231
M₃) σ: R →+* S
σ M: Type ?u.80222
M M₃: Type ?u.80231
M₃ where
  coe f: ?m.81471
f := f: ?m.81471
f.toFun: {M : Type ?u.81500} → {N : Type ?u.81499} → [inst : Add M] → [inst_1 : Add N] → AddHom M N → M → N
toFun
  coe_injective' f: ?m.81516
f g: ?m.81519
g h: ?m.81522
h := by
Goals accomplished! 🐙
    R: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

f, g: M →ₛₗ[σ] M₃

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcases f: M →ₛₗ[σ] M₃
fR: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

g: M →ₛₗ[σ] M₃

toAddHom✝: AddHom M M₃

map_smul'✝: ∀ (r : R) (x : M), AddHom.toFun toAddHom✝ (r • x) = ↑σ r • AddHom.toFun toAddHom✝ x

h: (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ } = (fun f => f.toFun) g

mk{ toAddHom := toAddHom✝, map_smul' := map_smul'✝ } = g
    R: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

f, g: M →ₛₗ[σ] M₃

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcases g: M →ₛₗ[σ] M₃
gR: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

toAddHom✝¹: AddHom M M₃

map_smul'✝¹: ∀ (r : R) (x : M), AddHom.toFun toAddHom✝¹ (r • x) = ↑σ r • AddHom.toFun toAddHom✝¹ x

toAddHom✝: AddHom M M₃

map_smul'✝: ∀ (r : R) (x : M), AddHom.toFun toAddHom✝ (r • x) = ↑σ r • AddHom.toFun toAddHom✝ x

h: (fun f => f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =   (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }

mk.mk{ toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } = { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
    R: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

f, g: M →ₛₗ[σ] M₃

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcongrR: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

toAddHom✝¹: AddHom M M₃

map_smul'✝¹: ∀ (r : R) (x : M), AddHom.toFun toAddHom✝¹ (r • x) = ↑σ r • AddHom.toFun toAddHom✝¹ x

toAddHom✝: AddHom M M₃

map_smul'✝: ∀ (r : R) (x : M), AddHom.toFun toAddHom✝ (r • x) = ↑σ r • AddHom.toFun toAddHom✝ x

h: (fun f => f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =   (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }

mk.mk.e_toAddHomtoAddHom✝¹ = toAddHom✝
    R: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

f, g: M →ₛₗ[σ] M₃

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gapply FunLike.coe_injective': ∀ {F : Sort ?u.82149} {α : outParam (Sort ?u.82148)} {β : outParam (α → Sort ?u.82147)} [self : FunLike F α β],
  Injective FunLike.coe
FunLike.coe_injective'R: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

toAddHom✝¹: AddHom M M₃

map_smul'✝¹: ∀ (r : R) (x : M), AddHom.toFun toAddHom✝¹ (r • x) = ↑σ r • AddHom.toFun toAddHom✝¹ x

toAddHom✝: AddHom M M₃

map_smul'✝: ∀ (r : R) (x : M), AddHom.toFun toAddHom✝ (r • x) = ↑σ r • AddHom.toFun toAddHom✝ x

h: (fun f => f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =   (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }

mk.mk.e_toAddHom.a↑toAddHom✝¹ = ↑toAddHom✝
    R: Type ?u.80198

R₁: Type ?u.80201

R₂: Type ?u.80204

R₃: Type ?u.80207

k: Type ?u.80210

S: Type ?u.80213

S₃: Type ?u.80216

T: Type ?u.80219

M: Type ?u.80222

M₁: Type ?u.80225

M₂: Type ?u.80228

M₃: Type ?u.80231

N₁: Type ?u.80234

N₂: Type ?u.80237

N₃: Type ?u.80240

ι: Type ?u.80243

inst✝¹¹: Semiring R

inst✝¹⁰: Semiring S

inst✝⁹: AddCommMonoid M

inst✝⁸: AddCommMonoid M₁

inst✝⁷: AddCommMonoid M₂

inst✝⁶: AddCommMonoid M₃

inst✝⁵: AddCommMonoid N₁

inst✝⁴: AddCommMonoid N₂

inst✝³: AddCommMonoid N₃

inst✝²: Module R M

inst✝¹: Module R M₂

inst✝: Module S M₃

σ: R →+* S

f, g: M →ₛₗ[σ] M₃

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gexact h: (fun f => f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =   (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
h
Goals accomplished! 🐙
  map_add f: ?m.81535
f := f: ?m.81535
f.map_add': ∀ {M : Type ?u.81553} {N : Type ?u.81552} [inst : Add M] [inst_1 : Add N] (self : AddHom M N) (x y : M),
  AddHom.toFun self (x + y) = AddHom.toFun self x + AddHom.toFun self y
map_add'
  map_smulₛₗ := LinearMap.map_smul': ∀ {R : Type ?u.81582} {S : Type ?u.81581} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type ?u.81580}
  {M₂ : Type ?u.81579} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module S M₂] (self : M →ₛₗ[σ] M₂) (r : R) (x : M),
  AddHom.toFun self.toAddHom (r • x) = ↑σ r • AddHom.toFun self.toAddHom x
LinearMap.map_smul'
#align linear_map.semilinear_map_class LinearMap.semilinearMapClass: {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {M₃ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] → [inst_5 : Module S M₃] → {σ : R →+* S} → SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
LinearMap.semilinearMapClass

-- Porting note: we don't port specialized `CoeFun` instances if there is `FunLike` instead
#noalign LinearMap.has_coe_to_fun

-- Porting note: adding this instance prevents a timeout in `ext_ring_op`
instance: {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {M₃ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] → [inst_5 : Module S M₃] → {σ : R →+* S} → FunLike (M →ₛₗ[σ] M₃) M fun x => M₃
instance {σ: R →+* S
σ : R: Type ?u.83905
R →+* S: Type ?u.83920
S} : FunLike: Sort ?u.84130 →
  (α : outParam (Sort ?u.84129)) → outParam (α → Sort ?u.84128) → Sort (max(max(max1?u.84130)?u.84129)?u.84128)
FunLike (M: Type ?u.83929
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.83938
M₃) M: Type ?u.83929
M (λ _: ?m.84240
_ ↦ M₃: Type ?u.83938
M₃) :=
  { AddHomClass.toFunLike with }: FunLike ?m.84401 ?m.84402 ?m.84403
{ AddHomClass.toFunLike: {F : Type ?u.84251} →
  {M : outParam (Type ?u.84250)} →
    {N : outParam (Type ?u.84249)} →
      [inst : Add M] → [inst_1 : Add N] → [self : AddHomClass F M N] → FunLike F M fun x => N
AddHomClass.toFunLike{ AddHomClass.toFunLike with }: FunLike ?m.84401 ?m.84402 ?m.84403
 { AddHomClass.toFunLike with }: FunLike ?m.84401 ?m.84402 ?m.84403
with{ AddHomClass.toFunLike with }: FunLike ?m.84401 ?m.84402 ?m.84403
 }

/-- The `DistribMulActionHom` underlying a `LinearMap`. -/
def toDistribMulActionHom: (M →ₗ[R] M₂) → M →+[R] M₂
toDistribMulActionHom (f: M →ₗ[R] M₂
f : M: Type ?u.85723
M →ₗ[R: Type ?u.85699
R] M₂: Type ?u.85729
M₂) : DistribMulActionHom: (M : Type ?u.86005) →
  [inst : Monoid M] →
    (A : Type ?u.86004) →
      [inst_1 : AddMonoid A] →
        [inst_2 : DistribMulAction M A] →
          (B : Type ?u.86003) → [inst_3 : AddMonoid B] → [inst : DistribMulAction M B] → Type (max?u.86004?u.86003)
DistribMulActionHom R: Type ?u.85699
R M: Type ?u.85723
M M₂: Type ?u.85729
M₂ :=
  { f: M →ₗ[R] M₂
f with map_zero' := show f: M →ₗ[R] M₂
f 0: ?m.89203
0 = 0: ?m.89665
0 from map_zero: ∀ {M : Type ?u.90296} {N : Type ?u.90297} {F : Type ?u.90295} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero f: M →ₗ[R] M₂
f }
#align linear_map.to_distrib_mul_action_hom LinearMap.toDistribMulActionHom: {R : Type u_1} →
  {M : Type u_2} →
    {M₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → (M →ₗ[R] M₂) → M →+[R] M₂
LinearMap.toDistribMulActionHom

@[simp]
theorem coe_toAddHom: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃), ↑f.toAddHom = ↑f
coe_toAddHom (f: M →ₛₗ[σ] M₃
f : M: Type ?u.92210
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.92219
M₃) : ⇑f: M →ₛₗ[σ] M₃
f.toAddHom: {R : Type ?u.92489} →
  {S : Type ?u.92488} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type ?u.92487} →
            {M₂ : Type ?u.92486} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] → [inst_5 : Module S M₂] → (M →ₛₗ[σ] M₂) → AddHom M M₂
toAddHom = f: M →ₛₗ[σ] M₃
f := rfl: ∀ {α : Sort ?u.94301} {a : α}, a = a
rfl

-- porting note: no longer a `simp`
theorem toFun_eq_coe: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f : M →ₛₗ[σ] M₃}, f.toFun = ↑f
toFun_eq_coe {f: M →ₛₗ[σ] M₃
f : M: Type ?u.94384
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.94393
M₃} : f: M →ₛₗ[σ] M₃
f.toFun: {M : Type ?u.94687} → {N : Type ?u.94686} → [inst : Add M] → [inst_1 : Add N] → AddHom M N → M → N
toFun = (f: M →ₛₗ[σ] M₃
f : M: Type ?u.94384
M → M₃: Type ?u.94393
M₃) := rfl: ∀ {α : Sort ?u.95733} {a : α}, a = a
rfl
#align linear_map.to_fun_eq_coe LinearMap.toFun_eq_coe: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f : M →ₛₗ[σ] M₃}, f.toFun = ↑f
LinearMap.toFun_eq_coe

@[ext]
theorem ext: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f g : M →ₛₗ[σ] M₃}, (∀ (x : M), ↑f x = ↑g x) → f = g
ext {f: M →ₛₗ[σ] M₃
f g: M →ₛₗ[σ] M₃
g : M: Type ?u.95778
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.95787
M₃} (h: ∀ (x : M), ↑f x = ↑g x
h : ∀ x: ?m.96100
x, f: M →ₛₗ[σ] M₃
f x: ?m.96100
x = g: M →ₛₗ[σ] M₃
g x: ?m.96100
x) : f: M →ₛₗ[σ] M₃
f = g: M →ₛₗ[σ] M₃
g :=
  FunLike.ext: ∀ {F : Sort ?u.96337} {α : Sort ?u.96338} {β : α → Sort ?u.96336} [i : FunLike F α β] (f g : F),
  (∀ (x : α), ↑f x = ↑g x) → f = g
FunLike.ext f: M →ₛₗ[σ] M₃
f g: M →ₛₗ[σ] M₃
g h: ∀ (x : M), ↑f x = ↑g x
h
#align linear_map.ext LinearMap.ext: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f g : M →ₛₗ[σ] M₃}, (∀ (x : M), ↑f x = ↑g x) → f = g
LinearMap.ext

/-- Copy of a `LinearMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy: (f : M →ₛₗ[σ] M₃) → (f' : M → M₃) → f' = ↑f → M →ₛₗ[σ] M₃
copy (f: M →ₛₗ[σ] M₃
f : M: Type ?u.96524
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.96533
M₃) (f': M → M₃
f' : M: Type ?u.96524
M → M₃: Type ?u.96533
M₃) (h: f' = ↑f
h : f': M → M₃
f' = ⇑f: M →ₛₗ[σ] M₃
f) : M: Type ?u.96524
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.96533
M₃
    where
  toFun := f': M → M₃
f'
  map_add' := h: f' = ↑f
h.symm: ∀ {α : Sort ?u.97923} {a b : α}, a = b → b = a
symm ▸ f: M →ₛₗ[σ] M₃
f.map_add': ∀ {M : Type ?u.97952} {N : Type ?u.97951} [inst : Add M] [inst_1 : Add N] (self : AddHom M N) (x y : M),
  AddHom.toFun self (x + y) = AddHom.toFun self x + AddHom.toFun self y
map_add'
  map_smul' := h: f' = ↑f
h.symm: ∀ {α : Sort ?u.97996} {a b : α}, a = b → b = a
symm ▸ f: M →ₛₗ[σ] M₃
f.map_smul': ∀ {R : Type ?u.98009} {S : Type ?u.98008} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type ?u.98007}
  {M₂ : Type ?u.98006} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module S M₂] (self : M →ₛₗ[σ] M₂) (r : R) (x : M),
  AddHom.toFun self.toAddHom (r • x) = ↑σ r • AddHom.toFun self.toAddHom x
map_smul'
#align linear_map.copy LinearMap.copy: {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {M₃ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module S M₃] → {σ : R →+* S} → (f : M →ₛₗ[σ] M₃) → (f' : M → M₃) → f' = ↑f → M →ₛₗ[σ] M₃
LinearMap.copy

@[simp]
theorem coe_copy: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ↑f), ↑(LinearMap.copy f f' h) = f'
coe_copy (f: M →ₛₗ[σ] M₃
f : M: Type ?u.98330
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.98339
M₃) (f': M → M₃
f' : M: Type ?u.98330
M → M₃: Type ?u.98339
M₃) (h: f' = ↑f
h : f': M → M₃
f' = ⇑f: M →ₛₗ[σ] M₃
f) : ⇑(f: M →ₛₗ[σ] M₃
f.copy: {R : Type ?u.98757} →
  {S : Type ?u.98756} →
    {M : Type ?u.98755} →
      {M₃ : Type ?u.98754} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module S M₃] → {σ : R →+* S} → (f : M →ₛₗ[σ] M₃) → (f' : M → M₃) → f' = ↑f → M →ₛₗ[σ] M₃
copy f': M → M₃
f' h: f' = ↑f
h) = f': M → M₃
f' :=
  rfl: ∀ {α : Sort ?u.98887} {a : α}, a = a
rfl
#align linear_map.coe_copy LinearMap.coe_copy: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ↑f), ↑(LinearMap.copy f f' h) = f'
LinearMap.coe_copy

theorem copy_eq: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ↑f), LinearMap.copy f f' h = f
copy_eq (f: M →ₛₗ[σ] M₃
f : M: Type ?u.98999
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.99008
M₃) (f': M → M₃
f' : M: Type ?u.98999
M → M₃: Type ?u.99008
M₃) (h: f' = ↑f
h : f': M → M₃
f' = ⇑f: M →ₛₗ[σ] M₃
f) : f: M →ₛₗ[σ] M₃
f.copy: {R : Type ?u.99426} →
  {S : Type ?u.99425} →
    {M : Type ?u.99424} →
      {M₃ : Type ?u.99423} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module S M₃] → {σ : R →+* S} → (f : M →ₛₗ[σ] M₃) → (f' : M → M₃) → f' = ↑f → M →ₛₗ[σ] M₃
copy f': M → M₃
f' h: f' = ↑f
h = f: M →ₛₗ[σ] M₃
f :=
  FunLike.ext': ∀ {F : Sort ?u.99465} {α : Sort ?u.99463} {β : α → Sort ?u.99464} [i : FunLike F α β] {f g : F}, ↑f = ↑g → f = g
FunLike.ext' h: f' = ↑f
h
#align linear_map.copy_eq LinearMap.copy_eq: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ↑f), LinearMap.copy f f' h = f
LinearMap.copy_eq

initialize_simps_projections LinearMap: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (R →+* S) →
          (M : Type u_3) →
            (M₂ : Type u_4) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (maxu_3u_4)
LinearMap (toFun: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (σ : R →+* S) →
          (M : Type u_3) →
            (M₂ : Type u_4) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst_4 : Module R M] → [inst_5 : Module S M₂] → (M →ₛₗ[σ] M₂) → M → M₂
toFun → apply: {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (σ : R →+* S) →
          (M : Type u_3) →
            (M₂ : Type u_4) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst_4 : Module R M] → [inst_5 : Module S M₂] → (M →ₛₗ[σ] M₂) → M → M₂
apply)

@[simp]
theorem coe_mk: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f x),
  ↑{ toAddHom := f, map_smul' := h } = ↑f
coe_mk {σ: R →+* S
σ : R: Type ?u.99904
R →+* S: Type ?u.99919
S} (f: AddHom M M₃
f : AddHom: (M : Type ?u.100128) → (N : Type ?u.100127) → [inst : Add M] → [inst : Add N] → Type (max?u.100128?u.100127)
AddHom M: Type ?u.99928
M M₃: Type ?u.99937
M₃) (h: ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f x
h) :
    ((LinearMap.mk: {R : Type ?u.101154} →
  {S : Type ?u.101153} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type ?u.101152} →
            {M₂ : Type ?u.101151} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₂] →
                      (toAddHom : AddHom M M₂) →
                        (∀ (r : R) (x : M), AddHom.toFun toAddHom (r • x) = ↑σ r • AddHom.toFun toAddHom x) →
                          M →ₛₗ[σ] M₂
LinearMap.mk f: AddHom M M₃
f h: ?m.101039
h : M: Type ?u.99928
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.99937
M₃) : M: Type ?u.99928
M → M₃: Type ?u.99937
M₃) = f: AddHom M M₃
f :=
  rfl: ∀ {α : Sort ?u.104376} {a : α}, a = a
rfl
#align linear_map.coe_mk LinearMap.coe_mk: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f x),
  ↑{ toAddHom := f, map_smul' := h } = ↑f
LinearMap.coe_mk

-- Porting note: This theorem is new.
@[simp]
theorem coe_addHom_mk: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f x),
  ↑{ toAddHom := f, map_smul' := h } = f
coe_addHom_mk {σ: R →+* S
σ : R: Type ?u.104464
R →+* S: Type ?u.104479
S} (f: AddHom M M₃
f : AddHom: (M : Type ?u.104688) → (N : Type ?u.104687) → [inst : Add M] → [inst : Add N] → Type (max?u.104688?u.104687)
AddHom M: Type ?u.104488
M M₃: Type ?u.104497
M₃) (h: ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f x
h) :
    ((LinearMap.mk: {R : Type ?u.105716} →
  {S : Type ?u.105715} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type ?u.105714} →
            {M₂ : Type ?u.105713} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₂] →
                      (toAddHom : AddHom M M₂) →
                        (∀ (r : R) (x : M), AddHom.toFun toAddHom (r • x) = ↑σ r • AddHom.toFun toAddHom x) →
                          M →ₛₗ[σ] M₂
LinearMap.mk f: AddHom M M₃
f h: ?m.105599
h : M: Type ?u.104488
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.104497
M₃) : AddHom: (M : Type ?u.105605) → (N : Type ?u.105604) → [inst : Add M] → [inst : Add N] → Type (max?u.105605?u.105604)
AddHom M: Type ?u.104488
M M₃: Type ?u.104497
M₃) = f: AddHom M M₃
f :=
  rfl: ∀ {α : Sort ?u.106091} {a : α}, a = a
rfl

/-- Identity map as a `LinearMap` -/
def id: M →ₗ[R] M
id : M: Type ?u.106198
M →ₗ[R: Type ?u.106174
R] M: Type ?u.106198
M :=
  { DistribMulActionHom.id: (M : Type ?u.106459) →
  [inst : Monoid M] → {A : Type ?u.106458} → [inst_1 : AddMonoid A] → [inst_2 : DistribMulAction M A] → A →+[M] A
DistribMulActionHom.id R: Type ?u.106174
R with toFun := _root_.id: {α : Sort ?u.107071} → α → α
_root_.id }
#align linear_map.id LinearMap.id: {R : Type u_1} → {M : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] M
LinearMap.id

theorem id_apply: ∀ (x : M), ↑id x = x
id_apply (x: M
x : M: Type ?u.108407
M) : @id: {R : Type ?u.108572} →
  {M : Type ?u.108571} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] M
id R: Type ?u.108383
R M: Type ?u.108407
M _ _ _ x: M
x = x: M
x :=
  rfl: ∀ {α : Sort ?u.108734} {a : α}, a = a
rfl
#align linear_map.id_apply LinearMap.id_apply: ∀ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M), ↑id x = x
LinearMap.id_apply

@[simp, norm_cast]
theorem id_coe: ↑id = _root_.id
id_coe : ((LinearMap.id: {R : Type ?u.109037} →
  {M : Type ?u.109036} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] M
LinearMap.id : M: Type ?u.108774
M →ₗ[R: Type ?u.108750
R] M: Type ?u.108774
M) : M: Type ?u.108774
M → M: Type ?u.108774
M) = _root_.id: {α : Sort ?u.109222} → α → α
_root_.id :=
  rfl: ∀ {α : Sort ?u.109268} {a : α}, a = a
rfl
#align linear_map.id_coe LinearMap.id_coe: ∀ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ↑id = _root_.id
LinearMap.id_coe

end

section

variable [AddCommMonoid: Type ?u.155474 → Type ?u.155474
AddCommMonoid M: Type ?u.109469
M] [AddCommMonoid: Type ?u.178141 → Type ?u.178141
AddCommMonoid M₁: Type ?u.129654
M₁] [AddCommMonoid: Type ?u.109797 → Type ?u.109797
AddCommMonoid M₂: Type ?u.169594
M₂] [AddCommMonoid: Type ?u.169160 → Type ?u.169160
AddCommMonoid M₃: Type ?u.109478
M₃]

variable [AddCommMonoid: Type ?u.169163 → Type ?u.169163
AddCommMonoid N₁: Type ?u.109547
N₁] [AddCommMonoid: Type ?u.139995 → Type ?u.139995
AddCommMonoid N₂: Type ?u.155459
N₂] [AddCommMonoid: Type ?u.145410 → Type ?u.145410
AddCommMonoid N₃: Type ?u.109553
N₃]

variable [Module: (R : Type ?u.134335) →
  (M : Type ?u.134334) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.134335?u.134334)
Module R: Type ?u.155420
R M: Type ?u.109761
M] [Module: (R : Type ?u.144970) →
  (M : Type ?u.144969) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.144970?u.144969)
Module R: Type ?u.109586
R M₂: Type ?u.109616
M₂] [Module: (R : Type ?u.109712) →
  (M : Type ?u.109711) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.109712?u.109711)
Module S: Type ?u.109601
S M₃: Type ?u.109619
M₃]

variable (σ: R →+* S
σ : R: Type ?u.109922
R →+* S: Type ?u.109752
S)

variable (fₗ: M →ₗ[R] M₂
fₗ gₗ: M →ₗ[R] M₂
gₗ : M: Type ?u.109946
M →ₗ[R: Type ?u.109922
R] M₂: Type ?u.194556
M₂) (f: M →ₛₗ[σ] M₃
f g: M →ₛₗ[σ] M₃
g : M: Type ?u.109946
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.109955
M₃)

theorem isLinear: IsLinearMap R ↑fₗ
isLinear : IsLinearMap: (R : Type ?u.110836) →
  {M : Type ?u.110835} →
    {M₂ : Type ?u.110834} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst : Module R M₂] → (M → M₂) → Prop
IsLinearMap R: Type ?u.110378
R fₗ: M →ₗ[R] M₂
fₗ :=
  ⟨fₗ: M →ₗ[R] M₂
fₗ.map_add': ∀ {M : Type ?u.111248} {N : Type ?u.111247} [inst : Add M] [inst_1 : Add N] (self : AddHom M N) (x y : M),
  AddHom.toFun self (x + y) = AddHom.toFun self x + AddHom.toFun self y
map_add', fₗ: M →ₗ[R] M₂
fₗ.map_smul': ∀ {R : Type ?u.112173} {S : Type ?u.112172} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type ?u.112171}
  {M₂ : Type ?u.112170} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module S M₂] (self : M →ₛₗ[σ] M₂) (r : R) (x : M),
  AddHom.toFun self.toAddHom (r • x) = ↑σ r • AddHom.toFun self.toAddHom x
map_smul'⟩
#align linear_map.is_linear LinearMap.isLinear: ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (fₗ : M →ₗ[R] M₂), IsLinearMap R ↑fₗ
LinearMap.isLinear

variable {fₗ: ?m.112663
fₗ gₗ: ?m.112666
gₗ f: ?m.112669
f g: ?m.112672
g σ: ?m.112675
σ}

theorem coe_injective: Injective FunLike.coe
coe_injective : Injective: {α : Sort ?u.113135} → {β : Sort ?u.113134} → (α → β) → Prop
Injective (FunLike.coe: {F : Sort ?u.113256} →
  {α : outParam (Sort ?u.113255)} → {β : outParam (α → Sort ?u.113254)} → [self : FunLike F α β] → F → (a : α) → β a
FunLike.coe : (M: Type ?u.112702
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.112711
M₃) → _: Sort ?u.113252
_) :=
  FunLike.coe_injective: ∀ {F : Sort ?u.113420} {α : Sort ?u.113421} {β : α → Sort ?u.113422} [i : FunLike F α β], Injective fun f => ↑f
FunLike.coe_injective
#align linear_map.coe_injective LinearMap.coe_injective: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S},
  Injective FunLike.coe
LinearMap.coe_injective

protected theorem congr_arg: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f : M →ₛₗ[σ] M₃} {x x' : M}, x = x' → ↑f x = ↑f x'
congr_arg {x: M
x x': M
x' : M: Type ?u.113632
M} : x: M
x = x': M
x' → f: M →ₛₗ[σ] M₃
f x: M
x = f: M →ₛₗ[σ] M₃
f x': M
x' :=
  FunLike.congr_arg: ∀ {F : Sort ?u.114318} {α : Sort ?u.114316} {β : Sort ?u.114317} [i : FunLike F α fun x => β] (f : F) {x y : α},
  x = y → ↑f x = ↑f y
FunLike.congr_arg f: M →ₛₗ[σ] M₃
f
#align linear_map.congr_arg LinearMap.congr_arg: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f : M →ₛₗ[σ] M₃} {x x' : M}, x = x' → ↑f x = ↑f x'
LinearMap.congr_arg

/-- If two linear maps are equal, they are equal at each point. -/
protected theorem congr_fun: f = g → ∀ (x : M), ↑f x = ↑g x
congr_fun (h: f = g
h : f: M →ₛₗ[σ] M₃
f = g: M →ₛₗ[σ] M₃
g) (x: M
x : M: Type ?u.114488
M) : f: M →ₛₗ[σ] M₃
f x: M
x = g: M →ₛₗ[σ] M₃
g x: M
x :=
  FunLike.congr_fun: ∀ {F : Sort ?u.115170} {α : Sort ?u.115172} {β : α → Sort ?u.115171} [i : FunLike F α β] {f g : F},
  f = g → ∀ (x : α), ↑f x = ↑g x
FunLike.congr_fun h: f = g
h x: M
x
#align linear_map.congr_fun LinearMap.congr_fun: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f g : M →ₛₗ[σ] M₃}, f = g → ∀ (x : M), ↑f x = ↑g x
LinearMap.congr_fun

theorem ext_iff: f = g ↔ ∀ (x : M), ↑f x = ↑g x
ext_iff : f: M →ₛₗ[σ] M₃
f = g: M →ₛₗ[σ] M₃
g ↔ ∀ x: ?m.115791
x, f: M →ₛₗ[σ] M₃
f x: ?m.115791
x = g: M →ₛₗ[σ] M₃
g x: ?m.115791
x :=
  FunLike.ext_iff: ∀ {F : Sort ?u.116026} {α : Sort ?u.116028} {β : α → Sort ?u.116027} [i : FunLike F α β] {f g : F},
  f = g ↔ ∀ (x : α), ↑f x = ↑g x
FunLike.ext_iff
#align linear_map.ext_iff LinearMap.ext_iff: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f g : M →ₛₗ[σ] M₃}, f = g ↔ ∀ (x : M), ↑f x = ↑g x
LinearMap.ext_iff

@[simp]
theorem mk_coe: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (h : ∀ (r : R) (x : M), AddHom.toFun (↑f) (r • x) = ↑σ r • AddHom.toFun (↑f) x),
  { toAddHom := ↑f, map_smul' := h } = f
mk_coe (f: M →ₛₗ[σ] M₃
f : M: Type ?u.116258
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.116267
M₃) (h: ∀ (r : R) (x : M), AddHom.toFun (↑f) (r • x) = ↑σ r • AddHom.toFun (↑f) x
h) : (LinearMap.mk: {R : Type ?u.116856} →
  {S : Type ?u.116855} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type ?u.116854} →
            {M₂ : Type ?u.116853} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₂] →
                      (toAddHom : AddHom M M₂) →
                        (∀ (r : R) (x : M), AddHom.toFun toAddHom (r • x) = ↑σ r • AddHom.toFun toAddHom x) →
                          M →ₛₗ[σ] M₂
LinearMap.mk f: M →ₛₗ[σ] M₃
f h: ?m.116804
h : M: Type ?u.116258
M →ₛₗ[σ: R →+* S
σ] M₃: Type ?u.116267
M₃) = f: M →ₛₗ[σ] M₃
f :=
  ext: ∀ {R : Type ?u.117243} {S : Type ?u.117244} {M : Type ?u.117245} {M₃ : Type ?u.117246} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M]
  [inst_5 : Module S M₃] {σ : R →+* S} {f g : M →ₛₗ[σ] M₃}, (∀ (x : M), ↑f x = ↑g x) → f = g
ext fun _: ?m.117405
_ ↦ rfl: ∀ {α : Sort ?u.117407} {a : α}, a = a
rfl
#align linear_map.mk_coe LinearMap.mk_coe: ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (h : ∀ (r : R) (x : M), AddHom.toFun (↑f) (r • x) = ↑σ r • AddHom.toFun (↑f) x),
  { toAddHom := ↑f, map_smul' := h } = f
LinearMap.mk_coe

variable (fₗ: ?m.118000
fₗ gₗ: ?m.118003
gₗ f: ?m.118006
f g: ?m.118009
g)

protected theorem map_add: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₃ : Type u_1} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (x y : M), ↑f (x + y) = ↑f x + ↑f y
map_add (x: M
x y: M
y : M: Type ?u.118036
M) : f: M →ₛₗ[σ] M₃
f (x: M
x + y: M
y) = f: M →ₛₗ[σ] M₃
f x: M
x + f: M →ₛₗ[σ] M₃
f y: M
y :=
  map_add: ∀ {M : Type ?u.120708} {N : Type ?u.120709} {F : Type ?u.120707} [inst : Add M] [inst_1 : Add N]
  [inst_2 : AddHomClass F M N] (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y
map_add f: M →ₛₗ[σ] M₃
f x: M
x y: M
y
#align linear_map.map_add LinearMap.map_add: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₃ : Type u_1} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (x y : M), ↑f (x + y) = ↑f x + ↑f y
LinearMap.map_add

protected theorem map_zero: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₃ : Type u_1} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃), ↑f 0 = 0
map_zero : f: M →ₛₗ[σ] M₃
f 0: ?m.122428
0 = 0: ?m.123011
0 :=
  map_zero: ∀ {M : Type ?u.123762} {N : Type ?u.123763} {F : Type ?u.123761} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero f: M →ₛₗ[σ] M₃
f
#align linear_map.map_zero LinearMap.map_zero: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₃ : Type u_1} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃), ↑f 0 = 0
LinearMap.map_zero

-- Porting note: `simp` wasn't picking up `map_smulₛₗ` for `LinearMap`s without specifying
-- `map_smulₛₗ f`, so we marked this as `@[simp]` in Mathlib3.
-- For Mathlib4, let's try without the `@[simp]` attribute and hope it won't need to be re-enabled.
protected theorem map_smulₛₗ: ∀ (c : R) (x : M), ↑f (c • x) = ↑σ c • ↑f x
map_smulₛₗ (c: R
c : R: Type ?u.125890
R) (x: M
x : M: Type ?u.125914
M) : f: M →ₛₗ[σ] M₃
f (c: R
c • x: M
x) = σ: R →+* S
σ c: R
c • f: M →ₛₗ[σ] M₃
f x: M
x :=
  map_smulₛₗ: ∀ {F : Type ?u.129371} {R : outParam (Type ?u.129370)} {S : outParam (Type ?u.129369)} [inst : Semiring R]
  [inst_1 : Semiring S] {σ : outParam (R →+* S)} {M : outParam (Type ?u.129368)} {M₂ : outParam (Type ?u.129367)}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  [self : SemilinearMapClass F σ M M₂] (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x
map_smulₛₗ f: M →ₛₗ[σ] M₃
f c: R
c x: M
x
#align linear_map.map_smulₛₗ LinearMap.map_smulₛₗ: ∀ {R : Type u_2} {S : Type u_4} {M : Type u_3} {M₃ : Type u_1} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (c : R) (x : M), ↑f (c • x) = ↑σ c • ↑f x
LinearMap.map_smulₛₗ

protected theorem map_smul: ∀ (c : R) (x : M), ↑fₗ (c • x) = c • ↑fₗ x
map_smul (c: R
c : R: Type ?u.129627
R) (x: M
x : M: Type ?u.129651
M) : fₗ: M →ₗ[R] M₂
fₗ (c: R
c • x: M
x) = c: R
c • fₗ: M →ₗ[R] M₂
fₗ x: M
x :=
  map_smul: ∀ {F : Type ?u.132134} {M : outParam (Type ?u.132133)} {X : outParam (Type ?u.132132)} {Y : outParam (Type ?u.132131)}
  [inst : SMul M X] [inst_1 : SMul M Y] [self : SMulHomClass F M X Y] (f : F) (c : M) (x : X), ↑f (c • x) = c • ↑f x
map_smul fₗ: M →ₗ[R] M₂
fₗ c: R
c x: M
x
#align linear_map.map_smul LinearMap.map_smul: ∀ {R : Type u_2} {M : Type u_3} {M₂ : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (fₗ : M →ₗ[R] M₂) (c : R) (x : M),
  ↑fₗ (c • x) = c • ↑fₗ x
LinearMap.map_smul

protected theorem map_smul_inv: ∀ {σ' : S →+* R} [inst : RingHomInvPair σ σ'] (c : S) (x : M), c • ↑f x = ↑f (↑σ' c • x)
map_smul_inv {σ': S →+* R
σ' : S: Type ?u.134274
S →+* R: Type ?u.134259
R} [RingHomInvPair: {R₁ : Type ?u.134754} →
  {R₂ : Type ?u.134753} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → (R₁ →+* R₂) → outParam (R₂ →+* R₁) → Prop
RingHomInvPair σ: R →+* S
σ σ': S →+* R
σ'] (c: S
c : S: Type ?u.134274
S) (x: M
x : M: Type ?u.134283
M) :
    c: S
c • f: M →ₛₗ[σ] M₃
f x: M
x = f: M →ₛₗ[σ] M₃
f (σ': S →+* R
σ' c: S
c • x: M
x) := by
Goals accomplished! 🐙 R: Type u_2

R₁: Type ?u.134262

R₂: Type ?u.134265

R₃: Type ?u.134268

k: Type ?u.134271

S: Type u_1

S₃: Type ?u.134277

T: Type ?u.134280

M: Type u_4

M₁: Type ?u.134286

M₂: Type ?u.134289

M₃: Type u_3

N₁: Type ?u.134295

N₂: Type ?u.134298

N₃: Type ?u.134301

ι: Type ?u.134304

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

σ': S →+* R

inst✝: RingHomInvPair σ σ'

c: S

x: M

c • ↑f x = ↑f (↑σ' c • x)simp
Goals accomplished! 🐙
#align linear_map.map_smul_inv LinearMap.map_smul_inv: ∀ {R : Type u_2} {S : Type u_1} {M : Type u_4} {M₃ : Type u_3} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] (c : S) (x : M), c • ↑f x = ↑f (↑σ' c • x)
LinearMap.map_smul_inv

@[simp]
theorem map_eq_zero_iff: Injective ↑f → ∀ {x : M}, ↑f x = 0 ↔ x = 0
map_eq_zero_iff (h: Injective ↑f
h : Function.Injective: {α : Sort ?u.140383} → {β : Sort ?u.140382} → (α → β) → Prop
Function.Injective f: M →ₛₗ[σ] M₃
f) {x: M
x : M: Type ?u.139950
M} : f: M →ₛₗ[σ] M₃
f x: M
x = 0: ?m.140632
0 ↔ x: M
x = 0: ?m.141383
0 :=
  _root_.map_eq_zero_iff: ∀ {M : Type ?u.141983} {N : Type ?u.141984} {F : Type ?u.141982} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), Injective ↑f → ∀ {x : M}, ↑f x = 0 ↔ x = 0
_root_.map_eq_zero_iff f: M →ₛₗ[σ] M₃
f h: Injective ↑f
h
#align linear_map.map_eq_zero_iff LinearMap.map_eq_zero_iff: ∀ {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃), Injective ↑f → ∀ {x : M}, ↑f x = 0 ↔ x = 0
LinearMap.map_eq_zero_iff

section Pointwise

open Pointwise

variable (M: ?m.145324
M M₃: ?m.145327
M₃ σ: ?m.145330
σ) {F: Type ?u.145333
F : Type _: Type (?u.155876+1)
Type _} (h: F
h : F: Type ?u.145333
F)

@[simp]
theorem _root_.image_smul_setₛₗ: ∀ {R : Type u_2} {S : Type u_3} (M : Type u_4) (M₃ : Type u_5) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] (σ : R →+* S)
  {F : Type u_1} (h : F) [inst_6 : SemilinearMapClass F σ M M₃] (c : R) (s : Set M), ↑h '' (c • s) = ↑σ c • ↑h '' s
_root_.image_smul_setₛₗ [SemilinearMapClass: Type ?u.145803 →
  {R : outParam (Type ?u.145802)} →
    {S : outParam (Type ?u.145801)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type ?u.145800)) →
              (M₂ : outParam (Type ?u.145799)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst : Module R M] → [inst : Module S M₂] → Type (max(max?u.145803?u.145800)?u.145799)
SemilinearMapClass F: Type ?u.145794
F σ: R →+* S
σ M: Type ?u.145362
M M₃: Type ?u.145371
M₃] (c: R
c : R: Type ?u.145338
R) (s: Set M
s : Set: Type ?u.145888 → Type ?u.145888
Set M: Type ?u.145362
M) :
    h: F
h '' (c: R
c • s: Set M
s) = σ: R →+* S
σ c: R
c • h: F
h '' s: Set M
s := by
Goals accomplished! 🐙
  R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

↑h '' (c • s) = ↑σ c • ↑h '' sapply Set.Subset.antisymm: ∀ {α : Type ?u.151461} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
Set.Subset.antisymmR: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₁↑h '' (c • s) ⊆ ↑σ c • ↑h '' s
R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₂↑σ c • ↑h '' s ⊆ ↑h '' (c • s)
  R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

↑h '' (c • s) = ↑σ c • ↑h '' s·R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₁↑h '' (c • s) ⊆ ↑σ c • ↑h '' s R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₁↑h '' (c • s) ⊆ ↑σ c • ↑h '' s
R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₂↑σ c • ↑h '' s ⊆ ↑h '' (c • s)rintro x: M₃
x ⟨y, ⟨z, zs, rfl⟩, rfl⟩: y ∈ c • s ∧ ↑h y = x
⟨y: M
y⟨y, ⟨z, zs, rfl⟩, rfl⟩: y ∈ c • s ∧ ↑h y = x
, ⟨z, zs, rfl⟩: z ∈ s ∧ (fun x => c • x) z = y
⟨z: M
z⟨z, zs, rfl⟩: z ∈ s ∧ (fun x => c • x) z = y
, zs: z ∈ s
zs⟨z, zs, rfl⟩: z ∈ s ∧ (fun x => c • x) z = y
, rfl: (fun x => c • x) z = y
rfl⟨z, zs, rfl⟩: z ∈ s ∧ (fun x => c • x) z = y
⟩⟨y, ⟨z, zs, rfl⟩, rfl⟩: y ∈ c • s ∧ ↑h y = x
, rfl: unknown free variable '_uniq.151524'
rfl⟨y, ⟨z, zs, rfl⟩, rfl⟩: y ∈ c • s ∧ ↑h y = x
⟩R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

z: M

zs: z ∈ s

h₁.intro.intro.intro.intro↑h ((fun x => c • x) z) ∈ ↑σ c • ↑h '' s
    R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₁↑h '' (c • s) ⊆ ↑σ c • ↑h '' sexact ⟨h: F
h z: M
z, Set.mem_image_of_mem: ∀ {α : Type ?u.153061} {β : Type ?u.153062} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
Set.mem_image_of_mem _: ?m.153063 → ?m.153064
_ zs: z ∈ s
zs, (map_smulₛₗ: ∀ {F : Type ?u.153087} {R : outParam (Type ?u.153086)} {S : outParam (Type ?u.153085)} [inst : Semiring R]
  [inst_1 : Semiring S] {σ : outParam (R →+* S)} {M : outParam (Type ?u.153084)} {M₂ : outParam (Type ?u.153083)}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  [self : SemilinearMapClass F σ M M₂] (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x
map_smulₛₗ _: ?m.153088
_ _: ?m.153089
_ _: ?m.153094
_).symm: ∀ {α : Sort ?u.153248} {a b : α}, a = b → b = a
symm⟩
Goals accomplished! 🐙
  R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

↑h '' (c • s) = ↑σ c • ↑h '' s·R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₂↑σ c • ↑h '' s ⊆ ↑h '' (c • s) R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₂↑σ c • ↑h '' s ⊆ ↑h '' (c • s)rintro x: M₃
x ⟨y, ⟨z, hz, rfl⟩, rfl⟩: x ∈ ↑σ c • ↑h '' s
⟨y: M₃
y⟨y, ⟨z, hz, rfl⟩, rfl⟩: x ∈ ↑σ c • ↑h '' s
, ⟨z, hz, rfl⟩: y ∈ ↑h '' s
⟨z: M
z⟨z, hz, rfl⟩: y ∈ ↑h '' s
, hz: z ∈ s
hz⟨z, hz, rfl⟩: y ∈ ↑h '' s
, rfl: ↑h z = y
rfl⟨z, hz, rfl⟩: y ∈ ↑h '' s
⟩⟨y, ⟨z, hz, rfl⟩, rfl⟩: x ∈ ↑σ c • ↑h '' s
, rfl: unknown free variable '_uniq.153458'
rfl⟨y, ⟨z, hz, rfl⟩, rfl⟩: x ∈ ↑σ c • ↑h '' s
⟩R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

z: M

hz: z ∈ s

h₂.intro.intro.intro.intro(fun x => ↑σ c • x) (↑h z) ∈ ↑h '' (c • s)
    R: Type u_2

R₁: Type ?u.145341

R₂: Type ?u.145344

R₃: Type ?u.145347

k: Type ?u.145350

S: Type u_3

S₃: Type ?u.145356

T: Type ?u.145359

M: Type u_4

M₁: Type ?u.145365

M₂: Type ?u.145368

M₃: Type u_5

N₁: Type ?u.145374

N₂: Type ?u.145377

N₃: Type ?u.145380

ι: Type ?u.145383

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

s: Set M

h₂↑σ c • ↑h '' s ⊆ ↑h '' (c • s)exact (Set.mem_image: ∀ {α : Type ?u.153519} {β : Type ?u.153520} (f : α → β) (s : Set α) (y : β), y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y
Set.mem_image _: ?m.153521 → ?m.153522
_ _: Set ?m.153521
_ _: ?m.153522
_).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨c: R
c • z: M
z, Set.smul_mem_smul_set: ∀ {α : Type ?u.154382} {β : Type ?u.154381} [inst : SMul α β] {s : Set β} {a : α} {b : β}, b ∈ s → a • b ∈ a • s
Set.smul_mem_smul_set hz: z ∈ s
hz, map_smulₛₗ: ∀ {F : Type ?u.155069} {R : outParam (Type ?u.155068)} {S : outParam (Type ?u.155067)} [inst : Semiring R]
  [inst_1 : Semiring S] {σ : outParam (R →+* S)} {M : outParam (Type ?u.155066)} {M₂ : outParam (Type ?u.155065)}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  [self : SemilinearMapClass F σ M M₂] (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x
map_smulₛₗ _: ?m.155070
_ _: ?m.155071
_ _: ?m.155076
_⟩
Goals accomplished! 🐙
#align image_smul_setₛₗ image_smul_setₛₗ: ∀ {R : Type u_2} {S : Type u_3} (M : Type u_4) (M₃ : Type u_5) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] (σ : R →+* S)
  {F : Type u_1} (h : F) [inst_6 : SemilinearMapClass F σ M M₃] (c : R) (s : Set M), ↑h '' (c • s) = ↑σ c • ↑h '' s
image_smul_setₛₗ

theorem _root_.preimage_smul_setₛₗ: ∀ [inst : SemilinearMapClass F σ M M₃] {c : R}, IsUnit c → ∀ (s : Set M₃), ↑h ⁻¹' (↑σ c • s) = c • ↑h ⁻¹' s
_root_.preimage_smul_setₛₗ [SemilinearMapClass: Type ?u.155885 →
  {R : outParam (Type ?u.155884)} →
    {S : outParam (Type ?u.155883)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type ?u.155882)) →
              (M₂ : outParam (Type ?u.155881)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst : Module R M] → [inst : Module S M₂] → Type (max(max?u.155885?u.155882)?u.155881)
SemilinearMapClass F: Type ?u.155876
F σ: R →+* S
σ M: Type ?u.155444
M M₃: Type ?u.155453
M₃] {c: R
c : R: Type ?u.155420
R} (hc: IsUnit c
hc : IsUnit: {M : Type ?u.155970} → [inst : Monoid M] → M → Prop
IsUnit c: R
c)
    (s: Set M₃
s : Set: Type ?u.156024 → Type ?u.156024
Set M₃: Type ?u.155453
M₃) :
    h: F
h ⁻¹' (σ: R →+* S
σ c: R
c • s: Set M₃
s) = c: R
c • h: F
h ⁻¹' s: Set M₃
s := by
Goals accomplished! 🐙
  R: Type u_2

R₁: Type ?u.155423

R₂: Type ?u.155426

R₃: Type ?u.155429

k: Type ?u.155432

S: Type u_3

S₃: Type ?u.155438

T: Type ?u.155441

M: Type u_4

M₁: Type ?u.155447

M₂: Type ?u.155450

M₃: Type u_5

N₁: Type ?u.155456

N₂: Type ?u.155459

N₃: Type ?u.155462

ι: Type ?u.155465

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

hc: IsUnit c

s: Set M₃

↑h ⁻¹' (↑σ c • s) = c • ↑h ⁻¹' sapply Set.Subset.antisymm: ∀ {α : Type ?u.161595} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
Set.Subset.antisymmR: Type u_2

R₁: Type ?u.155423

R₂: Type ?u.155426

R₃: Type ?u.155429

k: Type ?u.155432

S: Type u_3

S₃: Type ?u.155438

T: Type ?u.155441

M: Type u_4

M₁: Type ?u.155447

M₂: Type ?u.155450

M₃: Type u_5

N₁: Type ?u.155456

N₂: Type ?u.155459

N₃: Type ?u.155462

ι: Type ?u.155465

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

hc: IsUnit c

s: Set M₃

h₁↑h ⁻¹' (↑σ c • s) ⊆ c • ↑h ⁻¹' s
R: Type u_2

R₁: Type ?u.155423

R₂: Type ?u.155426

R₃: Type ?u.155429

k: Type ?u.155432

S: Type u_3

S₃: Type ?u.155438

T: Type ?u.155441

M: Type u_4

M₁: Type ?u.155447

M₂: Type ?u.155450

M₃: Type u_5

N₁: Type ?u.155456

N₂: Type ?u.155459

N₃: Type ?u.155462

ι: Type ?u.155465

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R] M₂

f, g: M →ₛₗ[σ] M₃

F: Type u_1

h: F

inst✝: SemilinearMapClass F σ M M₃

c: R

hc: IsUnit c

s: Set M₃

h₂c • ↑h ⁻¹' s ⊆ ↑h ⁻¹' (↑σ c • s)
  R: Type u_2

R₁: Type ?u.155423

R₂: Type ?u.155426

R₃: Type ?u.155429

k: Type ?u.155432

S: Type u_3

S₃: Type ?u.155438

T: Type ?u.155441

M: Type u_4

M₁: Type ?u.155447

M₂: Type ?u.155450

M₃: Type u_5

N₁: Type ?u.155456

N₂: Type ?u.155459

N₃: Type ?u.155462

ι: Type ?u.155465

inst✝¹²: Semiring R

inst✝¹¹: Semiring S

inst✝¹⁰: AddCommMonoid M

inst✝⁹: AddCommMonoid M₁

inst✝⁸: AddCommMonoid M₂

inst✝⁷: AddCommMonoid M₃

inst✝⁶: AddCommMonoid N₁

inst✝⁵: AddCommMonoid N₂

inst✝⁴: AddCommMonoid N₃

inst✝³: Module R M

inst✝²: Module R M₂

inst✝¹: Module S M₃

σ: R →+* S

fₗ, gₗ: M →ₗ[R