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

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.263916R : Type _: Type (?u.264788+1)Type _} {R₁: Type ?u.17R₁ : Type _: Type (?u.205902+1)Type _} {R₂: Type ?u.20R₂ : Type _: Type (?u.266336+1)Type _} {R₃: Type ?u.23R₃ : Type _: Type (?u.263925+1)Type _}
variable {k: Type ?u.26k : Type _: Type (?u.733631+1)Type _} {S: Type ?u.263931S : Type _: Type (?u.708857+1)Type _} {S₃: Type ?u.266348S₃ : Type _: Type (?u.251139+1)Type _} {T: Type ?u.264809T : Type _: Type (?u.248973+1)Type _}
variable {M: Type ?u.62M : Type _: Type (?u.719274+1)Type _} {M₁: Type ?u.65M₁ : Type _: Type (?u.263943+1)Type _} {M₂: Type ?u.266360M₂ : Type _: Type (?u.526709+1)Type _} {M₃: Type ?u.107M₃ : Type _: Type (?u.264821+1)Type _}
variable {N₁: Type ?u.413026N₁ : Type _: Type (?u.423584+1)Type _} {N₂: Type ?u.3585N₂ : Type _: Type (?u.423587+1)Type _} {N₃: Type ?u.3588N₃ : 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_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst : Module R M₂] → (M → M₂) → PropIsLinearMap (R: Type uR : Type u: Type (u+1)Type u) {M: Type vM : Type v: Type (v+1)Type v} {M₂: Type wM₂ : Type w: Type (w+1)Type w} [Semiring: Type ?u.176 → Type ?u.176Semiring R: Type uR] [AddCommMonoid: Type ?u.179 → Type ?u.179AddCommMonoid M: Type vM]
[AddCommMonoid: Type ?u.182 → Type ?u.182AddCommMonoid M₂: Type wM₂] [Module: (R : Type ?u.186) → (M : Type ?u.185) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.186?u.185)Module R: Type uR M: Type vM] [Module: (R : Type ?u.212) → (M : Type ?u.211) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max?u.212?u.211)Module R: Type uR M₂: Type wM₂] (f: M → M₂f : M: Type vM → M₂: Type wM₂) : Prop: TypeProp 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 ymap_add : ∀ x: ?m.241x y: ?m.244y, f: M → M₂f (x: ?m.241x + y: ?m.244y) = f: M → M₂f x: ?m.241x + f: M → M₂f y: ?m.244y
/-- 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 xmap_smul : ∀ (c: Rc : R: Type uR) (x: ?m.1916x), f: M → M₂f (c: Rc • x: ?m.1916x) = c: Rc • f: M → M₂f x: ?m.1916x
#align is_linear_map IsLinearMap: (R : Type u) →
{M : Type v} →
{M₂ : Type w} →
[inst : Semiring R] →
[inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst : Module R M₂] → (M → M₂) → PropIsLinearMap

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_4 : Module R M] →
[inst_5 : Module S M₂] →
LinearMap σ M M₂LinearMap {R: Type ?u.3642R : Type _: Type (?u.3642+1)Type _} {S: Type ?u.3645S : Type _: Type (?u.3645+1)Type _} [Semiring: Type ?u.3648 → Type ?u.3648Semiring R: Type ?u.3642R] [Semiring: Type ?u.3651 → Type ?u.3651Semiring S: Type ?u.3645S] (σ: R →+* Sσ : R: Type ?u.3642R →+* S: Type ?u.3645S) (M: Type ?u.3692M : Type _: Type (?u.3692+1)Type _)
(M₂: Type ?u.3695M₂ : Type _: Type (?u.3695+1)Type _) [AddCommMonoid: Type ?u.3698 → Type ?u.3698AddCommMonoid M: Type ?u.3692M] [AddCommMonoid: Type ?u.3701 → Type ?u.3701AddCommMonoid M₂: Type ?u.3695M₂] [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.3642R M: Type ?u.3692M] [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.3645S M₂: Type ?u.3695M₂] 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.3692M M₂: Type ?u.3695M₂ 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 xmap_smul' : ∀ (r: Rr : R: Type ?u.3642R) (x: Mx : M: Type ?u.3692M), toFun: M → M₂toFun (r: Rr • x: Mx) = σ: R →+* Sσ r: Rr • toFun: M → M₂toFun x: Mx
#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_3 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (maxu_3u_4)LinearMap

/-- The `AddHom` underlying a `LinearMap`. -/
{S : Type u_2} →
[inst : Semiring R] →
[inst_1 : Semiring S] →
{σ : R →+* S} →
{M : Type u_3} →
{M₂ : Type u_4} →
[inst_4 : Module R M] → [inst_5 : Module S M₂] → LinearMap σ M M₂ → AddHom M M₂LinearMap.toAddHom
{S : Type u_2} →
[inst : Semiring R] →
[inst_1 : Semiring S] →
{σ : R →+* S} →
{M : Type u_3} →
{M₂ : Type u_4} →
[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.10079M " →ₛₗ[" σ: ?m.10086σ:25 "] " M₂: ?m.10070M₂: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_3 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (maxu_3u_4)LinearMap σ: ?m.10828σ M: ?m.10821M M₂: ?m.10070M₂

/-- `M →ₗ[R] N` is the type of `R`-linear maps from `M` to `N`. -/
-- mathport name: «expr →ₗ[ ] »
notation:25 M: ?m.18954M " →ₗ[" R: ?m.18961R:25 "] " M₂: ?m.16408M₂: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_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.16417R) M: ?m.20126M M₂: ?m.20803M₂

/-- `M →ₗ⋆[R] N` is the type of `R`-conjugate-linear maps from `M` to `N`. -/
-- mathport name: «expr →ₗ⋆[ ] »
notation:25 M: ?m.34342M " →ₗ⋆[" R: ?m.34349R:25 "] " M₂: ?m.34333M₂: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_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 →+* RstarRingEnd R: ?m.31843R) M: ?m.36198M M₂: ?m.36191M₂

/-- `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_4 : Module R M] →
[inst_5 : Module S M₂] →
(∀ (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x) → SemilinearMapClass F σ M M₂SemilinearMapClass (F: Type ?u.46983F : Type _: Type (?u.46983+1)Type _) {R: outParam (Type ?u.46987)R S: outParam (Type ?u.46991)S : outParam: Sort ?u.46986 → Sort ?u.46986outParam (Type _: Type (?u.46987+1)Type _)} [Semiring: Type ?u.46994 → Type ?u.46994Semiring R: outParam (Type ?u.46987)R] [Semiring: Type ?u.46997 → Type ?u.46997Semiring S: outParam (Type ?u.46991)S]
(σ: outParam (R →+* S)σ : outParam: Sort ?u.47000 → Sort ?u.47000outParam (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.47039outParam (Type _: Type (?u.47040+1)Type _)) [AddCommMonoid: Type ?u.47047 → Type ?u.47047AddCommMonoid M: outParam (Type ?u.47040)M] [AddCommMonoid: Type ?u.47050 → Type ?u.47050AddCommMonoid 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.46983F 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 xmap_smulₛₗ : ∀ (f: Ff : F: Type ?u.46983F) (r: Rr : R: outParam (Type ?u.46987)R) (x: Mx : M: outParam (Type ?u.47040)M), f: Ff (r: Rr • x: Mx) = σ: outParam (R →+* S)σ r: Rr • f: Ff x: Mx
#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 : 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`

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 xmap_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_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → ?m.50811 F R M M₂LinearMapClass (F: Type ?u.50736F : 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.50747outParam (Type _: Type (?u.50748+1)Type _)) [Semiring: Type ?u.50751 → Type ?u.50751Semiring R: outParam (Type ?u.50740)R] [AddCommMonoid: Type ?u.50754 → Type ?u.50754AddCommMonoid M: outParam (Type ?u.50744)M]
[AddCommMonoid: Type ?u.50757 → Type ?u.50757AddCommMonoid 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 : Module R M] → [inst : Module S M₂] → Type (max(max?u.50826?u.50823)?u.50822)SemilinearMapClass F: Type ?u.50736F (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_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.51588F : Type _: Type (?u.51168+1)Type _)
variable [Semiring: Type ?u.51249 → Type ?u.51249Semiring R: Type ?u.50994R] [Semiring: Type ?u.51252 → Type ?u.51252Semiring S: Type ?u.51009S]
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.51352R M: Type ?u.51376M] [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.51352R M₂: Type ?u.51382M₂] [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.51213S M₃: Type ?u.51231M₃]
variable {σ: R →+* Sσ : R: Type ?u.51540R →+* S: Type ?u.51367S}

-- 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_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 : Module R M] → [inst : Module S M₂] → Type (max(max?u.51732?u.51729)?u.51728)SemilinearMapClass F: Type ?u.51588F σ: R →+* Sσ M: Type ?u.51564M M₃: Type ?u.51573M₃] :
(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.51588F M: Type ?u.51564M M₃: Type ?u.51573M₃ :=
{ 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_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.54293f ↦ (f: ?m.54293f : M: Type ?u.51564M → M₃: Type ?u.51573M₃)
map_zero := fun f: ?m.57005f ↦
show f: ?m.57005f 0: ?m.580890 = 0: ?m.585750 by
rw [R: Type ?u.51540R₁: Type ?u.51543R₂: Type ?u.51546R₃: Type ?u.51549k: Type ?u.51552S: Type ?u.51555S₃: Type ?u.51558T: Type ?u.51561M: Type ?u.51564M₁: Type ?u.51567M₂: Type ?u.51570M₃: Type ?u.51573N₁: Type ?u.51576N₂: Type ?u.51579N₃: Type ?u.51582ι: Type ?u.51585F: Type ?u.51588inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sinst✝: 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 = 0zero_smul R: Type ?u.51540R (0: ?m.605570 : M: Type ?u.51564M),R: Type ?u.51540R₁: Type ?u.51543R₂: Type ?u.51546R₃: Type ?u.51549k: Type ?u.51552S: Type ?u.51555S₃: Type ?u.51558T: Type ?u.51561M: Type ?u.51564M₁: Type ?u.51567M₂: Type ?u.51570M₃: Type ?u.51573N₁: Type ?u.51576N₂: Type ?u.51579N₃: Type ?u.51582ι: Type ?u.51585F: Type ?u.51588inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sinst✝: SemilinearMapClass F σ M M₃src✝:= toAddHomClass: AddHomClass F M M₃f: F↑f (0 • 0) = 0 R: Type ?u.51540R₁: Type ?u.51543R₂: Type ?u.51546R₃: Type ?u.51549k: Type ?u.51552S: Type ?u.51555S₃: Type ?u.51558T: Type ?u.51561M: Type ?u.51564M₁: Type ?u.51567M₂: Type ?u.51570M₃: Type ?u.51573N₁: Type ?u.51576N₂: Type ?u.51579N₃: Type ?u.51582ι: Type ?u.51585F: Type ?u.51588inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sinst✝: 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 xmap_smulₛₗR: Type ?u.51540R₁: Type ?u.51543R₂: Type ?u.51546R₃: Type ?u.51549k: Type ?u.51552S: Type ?u.51555S₃: Type ?u.51558T: Type ?u.51561M: Type ?u.51564M₁: Type ?u.51567M₂: Type ?u.51570M₃: Type ?u.51573N₁: Type ?u.51576N₂: Type ?u.51579N₃: Type ?u.51582ι: Type ?u.51585F: Type ?u.51588inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sinst✝: SemilinearMapClass F σ M M₃src✝:= toAddHomClass: AddHomClass F M M₃f: F↑σ 0 • ↑f 0 = 0]R: Type ?u.51540R₁: Type ?u.51543R₂: Type ?u.51546R₃: Type ?u.51549k: Type ?u.51552S: Type ?u.51555S₃: Type ?u.51558T: Type ?u.51561M: Type ?u.51564M₁: Type ?u.51567M₂: Type ?u.51570M₃: Type ?u.51573N₁: Type ?u.51576N₂: Type ?u.51579N₃: Type ?u.51582ι: Type ?u.51585F: Type ?u.51588inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sinst✝: SemilinearMapClass F σ M M₃src✝:= toAddHomClass: AddHomClass F M M₃f: F↑σ 0 • ↑f 0 = 0
R: Type ?u.51540R₁: Type ?u.51543R₂: Type ?u.51546R₃: Type ?u.51549k: Type ?u.51552S: Type ?u.51555S₃: Type ?u.51558T: Type ?u.51561M: Type ?u.51564M₁: Type ?u.51567M₂: Type ?u.51570M₃: Type ?u.51573N₁: Type ?u.51576N₂: Type ?u.51579N₃: Type ?u.51582ι: Type ?u.51585F: Type ?u.51588inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sinst✝: SemilinearMapClass F σ M M₃src✝:= toAddHomClass: AddHomClass F M M₃f: F↑f 0 = 0simpGoals 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_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_3 : Module R M] → [inst : Module R M₂] → Type (max(max?u.64990?u.64988)?u.64987)LinearMapClass F: Type ?u.64847F R: Type ?u.64799R M: Type ?u.64823M M₂: Type ?u.64829M₂] :
DistribMulActionHomClass: Type ?u.65052 →
(M : outParam (Type ?u.65051)) →
(A : outParam (Type ?u.65050)) →
(B : outParam (Type ?u.65049)) →
[inst : Monoid M] →
[inst_3 : DistribMulAction M A] →
[inst : DistribMulAction M B] → Type (max(max?u.65052?u.65050)?u.65049)DistribMulActionHomClass F: Type ?u.64847F R: Type ?u.64799R M: Type ?u.64823M M₂: Type ?u.64829M₂ :=
{ 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_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.64847F with
coe := fun f: ?m.68292f ↦ (f: ?m.68292f : M: Type ?u.64823M → M₂: Type ?u.64829M₂)
map_smul := fun f: ?m.70805f c: ?m.70808c x: ?m.70811x ↦ byGoals accomplished! 🐙 R: Type ?u.64799R₁: Type ?u.64802R₂: Type ?u.64805R₃: Type ?u.64808k: Type ?u.64811S: Type ?u.64814S₃: Type ?u.64817T: Type ?u.64820M: Type ?u.64823M₁: Type ?u.64826M₂: Type ?u.64829M₃: Type ?u.64832N₁: Type ?u.64835N₂: Type ?u.64838N₃: Type ?u.64841ι: Type ?u.64844F: Type ?u.64847inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sinst✝: LinearMapClass F R M M₂src✝:= addMonoidHomClass F: AddMonoidHomClass F M M₂f: Fc: Rx: M↑f (c • x) = c • ↑f xrw [R: Type ?u.64799R₁: Type ?u.64802R₂: Type ?u.64805R₃: Type ?u.64808k: Type ?u.64811S: Type ?u.64814S₃: Type ?u.64817T: Type ?u.64820M: Type ?u.64823M₁: Type ?u.64826M₂: Type ?u.64829M₃: Type ?u.64832N₁: Type ?u.64835N₂: Type ?u.64838N₃: Type ?u.64841ι: Type ?u.64844F: Type ?u.64847inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sinst✝: LinearMapClass F R M M₂src✝:= addMonoidHomClass F: AddMonoidHomClass F M M₂f: Fc: Rx: 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₂]

variable {F: ?m.71969F} (f: Ff : F: ?m.71969F) [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 : Module R M] → [inst : Module S M₂] → Type (max(max?u.72247?u.72244)?u.72243)SemilinearMapClass F: ?m.71969F σ: R →+* Sσ M: Type ?u.71805M M₃: Type ?u.71814M₃]

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.72068S →+* R: Type ?u.72053R} [RingHomInvPair: {R₁ : Type ?u.72361} →
{R₂ : Type ?u.72360} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → (R₁ →+* R₂) → outParam (R₂ →+* R₁) → PropRingHomInvPair σ: R →+* Sσ σ': S →+* Rσ'] (c: Sc : S: Type ?u.72068S) (x: Mx : M: Type ?u.72077M) :
c: Sc • f: Ff x: Mx = f: Ff (σ': S →+* Rσ' c: Sc • x: Mx) := byGoals accomplished! 🐙 R: Type u_2R₁: Type ?u.72056R₂: Type ?u.72059R₃: Type ?u.72062k: Type ?u.72065S: Type u_1S₃: Type ?u.72071T: Type ?u.72074M: Type u_5M₁: Type ?u.72080M₂: Type ?u.72083M₃: Type u_3N₁: Type ?u.72089N₂: Type ?u.72092N₃: Type ?u.72095ι: Type ?u.72098F: Type u_4inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sf: Fi: SemilinearMapClass F σ M M₃σ': S →+* Rinst✝: RingHomInvPair σ σ'c: Sx: Mc • ↑f x = ↑f (↑σ' c • x)simpGoals 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

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

section

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.79862R M: Type ?u.98999M] [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.79862R M₂: Type ?u.79892M₂] [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.79877S M₃: Type ?u.79895M₃]

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

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 : Module R M] → [inst : Module S M₂] → Type (max(max?u.80387?u.80384)?u.80383)SemilinearMapClass (M: Type ?u.80222M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.80231M₃) σ: R →+* Sσ M: Type ?u.80222M M₃: Type ?u.80231M₃ where
coe f: ?m.81471f := f: ?m.81471f.toFun: {M : Type ?u.81500} → {N : Type ?u.81499} → [inst : Add M] → [inst_1 : Add N] → AddHom M N → M → NtoFun
coe_injective' f: ?m.81516f g: ?m.81519g h: ?m.81522h := byGoals accomplished! 🐙
R: Type ?u.80198R₁: Type ?u.80201R₂: Type ?u.80204R₃: Type ?u.80207k: Type ?u.80210S: Type ?u.80213S₃: Type ?u.80216T: Type ?u.80219M: Type ?u.80222M₁: Type ?u.80225M₂: Type ?u.80228M₃: Type ?u.80231N₁: Type ?u.80234N₂: Type ?u.80237N₃: Type ?u.80240ι: Type ?u.80243inst✝¹¹: Semiring Rinst✝¹⁰: Semiring Sinst✝⁹: AddCommMonoid Minst✝⁸: AddCommMonoid M₁inst✝⁷: AddCommMonoid M₂inst✝⁶: AddCommMonoid M₃inst✝⁵: AddCommMonoid N₁inst✝⁴: AddCommMonoid N₂inst✝³: AddCommMonoid N₃inst✝²: Module R Minst✝¹: Module R M₂inst✝: Module S M₃σ: R →+* Sf, g: M →ₛₗ[σ] M₃h: (fun f => f.toFun) f = (fun f => f.toFun) gf = gapply FunLike.coe_injective': ∀ {F : Sort ?u.82149} {α : outParam (Sort ?u.82148)} {β : outParam (α → Sort ?u.82147)} [self : FunLike F α β],
R: Type ?u.80198R₁: Type ?u.80201R₂: Type ?u.80204R₃: Type ?u.80207k: Type ?u.80210S: Type ?u.80213S₃: Type ?u.80216T: Type ?u.80219M: Type ?u.80222M₁: Type ?u.80225M₂: Type ?u.80228M₃: Type ?u.80231N₁: Type ?u.80234N₂: Type ?u.80237N₃: Type ?u.80240ι: Type ?u.80243inst✝¹¹: Semiring Rinst✝¹⁰: Semiring Sinst✝⁹: AddCommMonoid Minst✝⁸: AddCommMonoid M₁inst✝⁷: AddCommMonoid M₂inst✝⁶: AddCommMonoid M₃inst✝⁵: AddCommMonoid N₁inst✝⁴: AddCommMonoid N₂inst✝³: AddCommMonoid N₃inst✝²: Module R Minst✝¹: Module R M₂inst✝: Module S M₃σ: R →+* Sf, g: M →ₛₗ[σ] M₃h: (fun f => f.toFun) f = (fun f => f.toFun) gf = gexact h: (fun f => f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =   (fun f => f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }hGoals accomplished! 🐙
map_add f: ?m.81535f := f: ?m.81535f.map_add': ∀ {M : Type ?u.81553} {N : Type ?u.81552} [inst : Add M] [inst_1 : Add N] (self : AddHom M N) (x y : M),
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),
#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_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_4 : Module R M] → [inst_5 : Module S M₃] → {σ : R →+* S} → FunLike (M →ₛₗ[σ] M₃) M fun x => M₃instance {σ: R →+* Sσ : R: Type ?u.83905R →+* S: Type ?u.83920S} : 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.83929M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.83938M₃) M: Type ?u.83929M (λ _: ?m.84240_ ↦ M₃: Type ?u.83938M₃) :=
{ 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 => NAddHomClass.toFunLike{ AddHomClass.toFunLike with }: FunLike ?m.84401 ?m.84402 ?m.84403 { AddHomClass.toFunLike with }: FunLike ?m.84401 ?m.84402 ?m.84403with{ 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.85723M →ₗ[R: Type ?u.85699R] M₂: Type ?u.85729M₂) : DistribMulActionHom: (M : Type ?u.86005) →
[inst : Monoid M] →
(A : Type ?u.86004) →
[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.85699R M: Type ?u.85723M M₂: Type ?u.85729M₂ :=
{ f: M →ₗ[R] M₂f with map_zero' := show f: M →ₗ[R] M₂f 0: ?m.892030 = 0: ?m.896650 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 = 0map_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_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 = ↑fcoe_toAddHom (f: M →ₛₗ[σ] M₃f : M: Type ?u.92210M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.92219M₃) : ⇑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_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 = arfl

-- 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 = ↑ftoFun_eq_coe {f: M →ₛₗ[σ] M₃f : M: Type ?u.94384M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.94393M₃} : f: M →ₛₗ[σ] M₃f.toFun: {M : Type ?u.94687} → {N : Type ?u.94686} → [inst : Add M] → [inst_1 : Add N] → AddHom M N → M → NtoFun = (f: M →ₛₗ[σ] M₃f : M: Type ?u.94384M → M₃: Type ?u.94393M₃) := rfl: ∀ {α : Sort ?u.95733} {a : α}, a = arfl
#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 = ↑fLinearMap.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 = gext {f: M →ₛₗ[σ] M₃f g: M →ₛₗ[σ] M₃g : M: Type ?u.95778M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.95787M₃} (h: ∀ (x : M), ↑f x = ↑g xh : ∀ x: ?m.96100x, f: M →ₛₗ[σ] M₃f x: ?m.96100x = g: M →ₛₗ[σ] M₃g x: ?m.96100x) : 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 = gFunLike.ext f: M →ₛₗ[σ] M₃f g: M →ₛₗ[σ] M₃g h: ∀ (x : M), ↑f x = ↑g xh
#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 = gLinearMap.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.96524M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.96533M₃) (f': M → M₃f' : M: Type ?u.96524M → M₃: Type ?u.96533M₃) (h: f' = ↑fh : f': M → M₃f' = ⇑f: M →ₛₗ[σ] M₃f) : M: Type ?u.96524M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.96533M₃
where
toFun := f': M → M₃f'
map_add' := h: f' = ↑fh.symm: ∀ {α : Sort ?u.97923} {a b : α}, a = b → b = asymm ▸ 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),
map_smul' := h: f' = ↑fh.symm: ∀ {α : Sort ?u.97996} {a b : α}, a = b → b = asymm ▸ 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),
#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_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.98330M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.98339M₃) (f': M → M₃f' : M: Type ?u.98330M → M₃: Type ?u.98339M₃) (h: f' = ↑fh : 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_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' = ↑fh) = f': M → M₃f' :=
rfl: ∀ {α : Sort ?u.98887} {a : α}, a = arfl
#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 = fcopy_eq (f: M →ₛₗ[σ] M₃f : M: Type ?u.98999M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.99008M₃) (f': M → M₃f' : M: Type ?u.98999M → M₃: Type ?u.99008M₃) (h: f' = ↑fh : 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_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' = ↑fh = 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 = gFunLike.ext' h: f' = ↑fh
#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 = fLinearMap.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_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_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_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 } = ↑fcoe_mk {σ: R →+* Sσ : R: Type ?u.99904R →+* S: Type ?u.99919S} (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.99928M M₃: Type ?u.99937M₃) (h: ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f xh) :
((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_4 : Module R M] →
[inst_5 : Module S M₂] →
M →ₛₗ[σ] M₂LinearMap.mk f: AddHom M M₃f h: ?m.101039h : M: Type ?u.99928M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.99937M₃) : M: Type ?u.99928M → M₃: Type ?u.99937M₃) = f: AddHom M M₃f :=
rfl: ∀ {α : Sort ?u.104376} {a : α}, a = arfl
#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 } = ↑fLinearMap.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 } = fcoe_addHom_mk {σ: R →+* Sσ : R: Type ?u.104464R →+* S: Type ?u.104479S} (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.104488M M₃: Type ?u.104497M₃) (h: ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f xh) :
((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_4 : Module R M] →
[inst_5 : Module S M₂] →
M →ₛₗ[σ] M₂LinearMap.mk f: AddHom M M₃f h: ?m.105599h : M: Type ?u.104488M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.104497M₃) : 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.104488M M₃: Type ?u.104497M₃) = f: AddHom M M₃f :=
rfl: ∀ {α : Sort ?u.106091} {a : α}, a = arfl

/-- Identity map as a `LinearMap` -/
def id: M →ₗ[R] Mid : M: Type ?u.106198M →ₗ[R: Type ?u.106174R] M: Type ?u.106198M :=
{ DistribMulActionHom.id: (M : Type ?u.106459) →
[inst : Monoid M] → {A : Type ?u.106458} → [inst_1 : AddMonoid A] → [inst_2 : DistribMulAction M A] → A →+[M] ADistribMulActionHom.id R: Type ?u.106174R 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] MLinearMap.id

theorem id_apply: ∀ (x : M), ↑id x = xid_apply (x: Mx : M: Type ?u.108407M) : @id: {R : Type ?u.108572} →
{M : Type ?u.108571} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] Mid R: Type ?u.108383R M: Type ?u.108407M _ _ _ x: Mx = x: Mx :=
rfl: ∀ {α : Sort ?u.108734} {a : α}, a = arfl
#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 = xLinearMap.id_apply

@[simp, norm_cast]
theorem id_coe: ↑id = _root_.idid_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] MLinearMap.id : M: Type ?u.108774M →ₗ[R: Type ?u.108750R] M: Type ?u.108774M) : M: Type ?u.108774M → M: Type ?u.108774M) = _root_.id: {α : Sort ?u.109222} → α → α_root_.id :=
rfl: ∀ {α : Sort ?u.109268} {a : α}, a = arfl
#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_.idLinearMap.id_coe

end

section

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.155420R M: Type ?u.109761M] [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.109586R M₂: Type ?u.109616M₂] [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.109601S M₃: Type ?u.109619M₃]

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

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

theorem isLinear: IsLinearMap R ↑fₗisLinear : IsLinearMap: (R : Type ?u.110836) →
{M : Type ?u.110835} →
{M₂ : Type ?u.110834} →
[inst : Semiring R] →
[inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst : Module R M₂] → (M → M₂) → PropIsLinearMap R: Type ?u.110378R 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 ymap_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),
#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.112663fₗ gₗ: ?m.112666gₗ f: ?m.112669f g: ?m.112672g σ: ?m.112675σ}

theorem coe_injective: Injective FunLike.coecoe_injective : Injective: {α : Sort ?u.113135} → {β : Sort ?u.113134} → (α → β) → PropInjective (FunLike.coe: {F : Sort ?u.113256} →
{α : outParam (Sort ?u.113255)} → {β : outParam (α → Sort ?u.113254)} → [self : FunLike F α β] → F → (a : α) → β aFunLike.coe : (M: Type ?u.112702M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.112711M₃) → _: Sort ?u.113252_) :=
FunLike.coe_injective: ∀ {F : Sort ?u.113420} {α : Sort ?u.113421} {β : α → Sort ?u.113422} [i : FunLike F α β], Injective fun f => ↑fFunLike.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.coeLinearMap.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: Mx x': Mx' : M: Type ?u.113632M} : x: Mx = x': Mx' → f: M →ₛₗ[σ] M₃f x: Mx = f: M →ₛₗ[σ] M₃f x': Mx' :=
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 yFunLike.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 xcongr_fun (h: f = gh : f: M →ₛₗ[σ] M₃f = g: M →ₛₗ[σ] M₃g) (x: Mx : M: Type ?u.114488M) : f: M →ₛₗ[σ] M₃f x: Mx = g: M →ₛₗ[σ] M₃g x: Mx :=
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 xFunLike.congr_fun h: f = gh x: Mx
#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 xLinearMap.congr_fun

theorem ext_iff: f = g ↔ ∀ (x : M), ↑f x = ↑g xext_iff : f: M →ₛₗ[σ] M₃f = g: M →ₛₗ[σ] M₃g ↔ ∀ x: ?m.115791x, f: M →ₛₗ[σ] M₃f x: ?m.115791x = g: M →ₛₗ[σ] M₃g x: ?m.115791x :=
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 xFunLike.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 xLinearMap.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 } = fmk_coe (f: M →ₛₗ[σ] M₃f : M: Type ?u.116258M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.116267M₃) (h: ∀ (r : R) (x : M), AddHom.toFun (↑f) (r • x) = ↑σ r • AddHom.toFun (↑f) xh) : (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_4 : Module R M] →
[inst_5 : Module S M₂] →
M →ₛₗ[σ] M₂LinearMap.mk f: M →ₛₗ[σ] M₃f h: ?m.116804h : M: Type ?u.116258M →ₛₗ[σ: R →+* Sσ] M₃: Type ?u.116267M₃) = 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 = gext fun _: ?m.117405_ ↦ rfl: ∀ {α : Sort ?u.117407} {a : α}, a = arfl
#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 } = fLinearMap.mk_coe

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

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 ymap_add (x: Mx y: My : M: Type ?u.118036M) : f: M →ₛₗ[σ] M₃f (x: Mx + y: My) = f: M →ₛₗ[σ] M₃f x: Mx + f: M →ₛₗ[σ] M₃f y: My :=
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 ymap_add f: M →ₛₗ[σ] M₃f x: Mx y: My
#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 yLinearMap.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 = 0map_zero : f: M →ₛₗ[σ] M₃f 0: ?m.1224280 = 0: ?m.1230110 :=
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 = 0map_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 = 0LinearMap.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 xmap_smulₛₗ (c: Rc : R: Type ?u.125890R) (x: Mx : M: Type ?u.125914M) : f: M →ₛₗ[σ] M₃f (c: Rc • x: Mx) = σ: R →+* Sσ c: Rc • f: M →ₛₗ[σ] M₃f x: Mx :=
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 xmap_smulₛₗ f: M →ₛₗ[σ] M₃f c: Rc x: Mx
#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 xLinearMap.map_smulₛₗ

protected theorem map_smul: ∀ (c : R) (x : M), ↑fₗ (c • x) = c • ↑fₗ xmap_smul (c: Rc : R: Type ?u.129627R) (x: Mx : M: Type ?u.129651M) : fₗ: M →ₗ[R] M₂fₗ (c: Rc • x: Mx) = c: Rc • fₗ: M →ₗ[R] M₂fₗ x: Mx :=
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 xmap_smul fₗ: M →ₗ[R] M₂fₗ c: Rc x: Mx
#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ₗ xLinearMap.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.134274S →+* R: Type ?u.134259R} [RingHomInvPair: {R₁ : Type ?u.134754} →
{R₂ : Type ?u.134753} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → (R₁ →+* R₂) → outParam (R₂ →+* R₁) → PropRingHomInvPair σ: R →+* Sσ σ': S →+* Rσ'] (c: Sc : S: Type ?u.134274S) (x: Mx : M: Type ?u.134283M) :
c: Sc • f: M →ₛₗ[σ] M₃f x: Mx = f: M →ₛₗ[σ] M₃f (σ': S →+* Rσ' c: Sc • x: Mx) := byGoals accomplished! 🐙 R: Type u_2R₁: Type ?u.134262R₂: Type ?u.134265R₃: Type ?u.134268k: Type ?u.134271S: Type u_1S₃: Type ?u.134277T: Type ?u.134280M: Type u_4M₁: Type ?u.134286M₂: Type ?u.134289M₃: Type u_3N₁: Type ?u.134295N₂: Type ?u.134298N₃: Type ?u.134301ι: Type ?u.134304inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sfₗ, gₗ: M →ₗ[R] M₂f, g: M →ₛₗ[σ] M₃σ': S →+* Rinst✝: RingHomInvPair σ σ'c: Sx: Mc • ↑f x = ↑f (↑σ' c • x)simpGoals 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 = 0map_eq_zero_iff (h: Injective ↑fh : Function.Injective: {α : Sort ?u.140383} → {β : Sort ?u.140382} → (α → β) → PropFunction.Injective f: M →ₛₗ[σ] M₃f) {x: Mx : M: Type ?u.139950M} : f: M →ₛₗ[σ] M₃f x: Mx = 0: ?m.1406320 ↔ x: Mx = 0: ?m.1413830 :=
_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 ↑fh
#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 = 0LinearMap.map_eq_zero_iff

section Pointwise

open Pointwise

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

@[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 : Module R M] → [inst : Module S M₂] → Type (max(max?u.145803?u.145800)?u.145799)SemilinearMapClass F: Type ?u.145794F σ: R →+* Sσ M: Type ?u.145362M M₃: Type ?u.145371M₃] (c: Rc : R: Type ?u.145338R) (s: Set Ms : Set: Type ?u.145888 → Type ?u.145888Set M: Type ?u.145362M) :
h: Fh '' (c: Rc • s: Set Ms) = σ: R →+* Sσ c: Rc • h: Fh '' s: Set Ms := byGoals accomplished! 🐙
R: Type u_2R₁: Type ?u.145341R₂: Type ?u.145344R₃: Type ?u.145347k: Type ?u.145350S: Type u_3S₃: Type ?u.145356T: Type ?u.145359M: Type u_4M₁: Type ?u.145365M₂: Type ?u.145368M₃: Type u_5N₁: Type ?u.145374N₂: Type ?u.145377N₃: Type ?u.145380ι: Type ?u.145383inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sfₗ, gₗ: M →ₗ[R] M₂f, g: M →ₛₗ[σ] M₃F: Type u_1h: Finst✝: SemilinearMapClass F σ M M₃c: Rs: Set Mh₁↑h '' (c • s) ⊆ ↑σ c • ↑h '' sexact ⟨h: Fh z: Mz, Set.mem_image_of_mem: ∀ {α : Type ?u.153061} {β : Type ?u.153062} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' aSet.mem_image_of_mem _: ?m.153063 → ?m.153064_ zs: z ∈ szs, (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 xmap_smulₛₗ _: ?m.153088_ _: ?m.153089_ _: ?m.153094_).symm: ∀ {α : Sort ?u.153248} {a b : α}, a = b → b = asymm⟩Goals accomplished! 🐙
R: Type u_2R₁: Type ?u.145341R₂: Type ?u.145344R₃: Type ?u.145347k: Type ?u.145350S: Type u_3S₃: Type ?u.145356T: Type ?u.145359M: Type u_4M₁: Type ?u.145365M₂: Type ?u.145368M₃: Type u_5N₁: Type ?u.145374N₂: Type ?u.145377N₃: Type ?u.145380ι: Type ?u.145383inst✝¹²: Semiring Rinst✝¹¹: Semiring Sinst✝¹⁰: AddCommMonoid Minst✝⁹: AddCommMonoid M₁inst✝⁸: AddCommMonoid M₂inst✝⁷: AddCommMonoid M₃inst✝⁶: AddCommMonoid N₁inst✝⁵: AddCommMonoid N₂inst✝⁴: AddCommMonoid N₃inst✝³: Module R Minst✝²: Module R M₂inst✝¹: Module S M₃σ: R →+* Sfₗ, gₗ: M →ₗ[R] M₂f, g: M →ₛₗ[σ] M₃F: Type u_1h: Finst✝: SemilinearMapClass F σ M M₃c: Rs: Set Mh₂↑σ 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 = ySet.mem_image _: ?m.153521 → ?m.153522_ _: Set ?m.153521_ _: ?m.153522_).2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨c: Rc • z: Mz, Set.smul_mem_smul_set: ∀ {α : Type ?u.154382} {β : Type ?u.154381} [inst : SMul α β] {s : Set β} {a : α} {b : β}, b ∈ s → a • b ∈ a • sSet.smul_mem_smul_set hz: z ∈ shz, 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 xmap_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 '' simage_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)) →