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.
/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Patrick Massot

! This file was ported from Lean 3 source module group_theory.group_action.pi
! leanprover-community/mathlib commit bbeb185db4ccee8ed07dc48449414ebfa39cb821
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Pi
import Mathlib.GroupTheory.GroupAction.Defs

/-!
# Pi instances for multiplicative actions

This file defines instances for `MulAction` and related structures on `Pi` types.

## See also

* `GroupTheory.GroupAction.option`
* `GroupTheory.GroupAction.prod`
* `GroupTheory.GroupAction.sigma`
* `GroupTheory.GroupAction.sum`
-/


universe u v w

variable {
I: Type u
I
:
Type u: Type (u+1)
Type u
} -- The indexing type variable {
f: I β†’ Type v
f
:
I: Type u
I
β†’
Type v: Type (v+1)
Type v
} -- The family of types already equipped with instances variable (
x: (i : I) β†’ f i
x
y: (i : I) β†’ f i
y
: βˆ€
i: ?m.23
i
,
f: I β†’ Type v
f
i: ?m.17
i
) (
i: I
i
:
I: Type u
I
) namespace Pi @[
to_additive: {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ [inst : (i : I) β†’ VAdd (f i) (g i)] β†’ VAdd ((i : I) β†’ f i) ((i : I) β†’ g i)
to_additive
] instance
smul': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ [inst : (i : I) β†’ SMul (f i) (g i)] β†’ SMul ((i : I) β†’ f i) ((i : I) β†’ g i)
smul'
{
g: I β†’ Type ?u.52
g
:
I: Type u
I
β†’
Type _: Type (?u.52+1)
Type _
} [βˆ€
i: ?m.56
i
,
SMul: Type ?u.60 β†’ Type ?u.59 β†’ Type (max?u.60?u.59)
SMul
(
f: I β†’ Type v
f
i: ?m.56
i
) (
g: I β†’ Type ?u.52
g
i: ?m.56
i
)] :
SMul: Type ?u.65 β†’ Type ?u.64 β†’ Type (max?u.65?u.64)
SMul
(βˆ€
i: ?m.67
i
,
f: I β†’ Type v
f
i: ?m.67
i
) (βˆ€
i: I
i
:
I: Type u
I
,
g: I β†’ Type ?u.52
g
i: I
i
) := ⟨fun
s: ?m.91
s
x: ?m.94
x
=> fun
i: ?m.98
i
=>
s: ?m.91
s
i: ?m.98
i
β€’
x: ?m.94
x
i: ?m.98
i
⟩ #align pi.has_smul'
Pi.smul': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ [inst : (i : I) β†’ SMul (f i) (g i)] β†’ SMul ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.smul'
#align pi.has_vadd'
Pi.vadd': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ [inst : (i : I) β†’ VAdd (f i) (g i)] β†’ VAdd ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.vadd'
@[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} (i : I) {g : I β†’ Type u_1} [inst : (i : I) β†’ VAdd (f i) (g i)] (s : (i : I) β†’ f i) (x : (i : I) β†’ g i), (s +α΅₯ x) i = s i +α΅₯ x i
to_additive
(attr := simp)] theorem
smul_apply': βˆ€ {g : I β†’ Type u_1} [inst : (i : I) β†’ SMul (f i) (g i)] (s : (i : I) β†’ f i) (x : (i : I) β†’ g i), (s β€’ x) i = s i β€’ x i
smul_apply'
{
g: I β†’ Type ?u.477
g
:
I: Type u
I
β†’
Type _: Type (?u.477+1)
Type _
} [βˆ€
i: ?m.481
i
,
SMul: Type ?u.485 β†’ Type ?u.484 β†’ Type (max?u.485?u.484)
SMul
(
f: I β†’ Type v
f
i: ?m.481
i
) (
g: I β†’ Type ?u.477
g
i: ?m.481
i
)] (
s: (i : I) β†’ f i
s
: βˆ€
i: ?m.490
i
,
f: I β†’ Type v
f
i: ?m.490
i
) (
x: (i : I) β†’ g i
x
: βˆ€
i: ?m.496
i
,
g: I β†’ Type ?u.477
g
i: ?m.496
i
) : (
s: (i : I) β†’ f i
s
β€’
x: (i : I) β†’ g i
x
)
i: I
i
=
s: (i : I) β†’ f i
s
i: I
i
β€’
x: (i : I) β†’ g i
x
i: I
i
:=
rfl: βˆ€ {Ξ± : Sort ?u.629} {a : Ξ±}, a = a
rfl
#align pi.smul_apply'
Pi.smul_apply': βˆ€ {I : Type u} {f : I β†’ Type v} (i : I) {g : I β†’ Type u_1} [inst : (i : I) β†’ SMul (f i) (g i)] (s : (i : I) β†’ f i) (x : (i : I) β†’ g i), (s β€’ x) i = s i β€’ x i
Pi.smul_apply'
#align pi.vadd_apply'
Pi.vadd_apply': βˆ€ {I : Type u} {f : I β†’ Type v} (i : I) {g : I β†’ Type u_1} [inst : (i : I) β†’ VAdd (f i) (g i)] (s : (i : I) β†’ f i) (x : (i : I) β†’ g i), (s +α΅₯ x) i = s i +α΅₯ x i
Pi.vadd_apply'
-- Porting note: `to_additive` fails to correctly translate name @[to_additive
Pi.vaddAssocClass: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : VAdd Ξ± Ξ²] [inst_1 : (i : I) β†’ VAdd Ξ² (f i)] [inst_2 : (i : I) β†’ VAdd Ξ± (f i)] [inst_3 : βˆ€ (i : I), VAddAssocClass Ξ± Ξ² (f i)], VAddAssocClass Ξ± Ξ² ((i : I) β†’ f i)
Pi.vaddAssocClass
] instance
isScalarTower: βˆ€ {Ξ± : Type ?u.765} {Ξ² : Type ?u.768} [inst : SMul Ξ± Ξ²] [inst_1 : (i : I) β†’ SMul Ξ² (f i)] [inst_2 : (i : I) β†’ SMul Ξ± (f i)] [inst_3 : βˆ€ (i : I), IsScalarTower Ξ± Ξ² (f i)], IsScalarTower Ξ± Ξ² ((i : I) β†’ f i)
isScalarTower
{
Ξ±: Type ?u.765
Ξ±
Ξ²: Type ?u.768
Ξ²
:
Type _: Type (?u.768+1)
Type _
} [
SMul: Type ?u.772 β†’ Type ?u.771 β†’ Type (max?u.772?u.771)
SMul
Ξ±: Type ?u.765
Ξ±
Ξ²: Type ?u.768
Ξ²
] [βˆ€
i: ?m.776
i
,
SMul: Type ?u.780 β†’ Type ?u.779 β†’ Type (max?u.780?u.779)
SMul
Ξ²: Type ?u.768
Ξ²
<|
f: I β†’ Type v
f
i: ?m.776
i
] [βˆ€
i: ?m.785
i
,
SMul: Type ?u.789 β†’ Type ?u.788 β†’ Type (max?u.789?u.788)
SMul
Ξ±: Type ?u.765
Ξ±
<|
f: I β†’ Type v
f
i: ?m.785
i
] [βˆ€
i: ?m.794
i
,
IsScalarTower: (M : Type ?u.799) β†’ (N : Type ?u.798) β†’ (Ξ± : Type ?u.797) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower
Ξ±: Type ?u.765
Ξ±
Ξ²: Type ?u.768
Ξ²
(
f: I β†’ Type v
f
i: ?m.794
i
)] :
IsScalarTower: (M : Type ?u.850) β†’ (N : Type ?u.849) β†’ (Ξ± : Type ?u.848) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower
Ξ±: Type ?u.765
Ξ±
Ξ²: Type ?u.768
Ξ²
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
) := ⟨fun
x: ?m.1060
x
y: ?m.1063
y
z: ?m.1066
z
=>
funext: βˆ€ {Ξ± : Sort ?u.1069} {Ξ² : Ξ± β†’ Sort ?u.1068} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
i: ?m.1083
i
=>
smul_assoc: βˆ€ {Ξ± : Type ?u.1087} {M : Type ?u.1085} {N : Type ?u.1086} [inst : SMul M N] [inst_1 : SMul N Ξ±] [inst_2 : SMul M Ξ±] [inst_3 : IsScalarTower M N Ξ±] (x : M) (y : N) (z : Ξ±), (x β€’ y) β€’ z = x β€’ y β€’ z
smul_assoc
x: ?m.1060
x
y: ?m.1063
y
(
z: ?m.1066
z
i: ?m.1083
i
)⟩ #align pi.is_scalar_tower
Pi.isScalarTower: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : SMul Ξ± Ξ²] [inst_1 : (i : I) β†’ SMul Ξ² (f i)] [inst_2 : (i : I) β†’ SMul Ξ± (f i)] [inst_3 : βˆ€ (i : I), IsScalarTower Ξ± Ξ² (f i)], IsScalarTower Ξ± Ξ² ((i : I) β†’ f i)
Pi.isScalarTower
#align pi.vadd_assoc_class
Pi.vaddAssocClass: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : VAdd Ξ± Ξ²] [inst_1 : (i : I) β†’ VAdd Ξ² (f i)] [inst_2 : (i : I) β†’ VAdd Ξ± (f i)] [inst_3 : βˆ€ (i : I), VAddAssocClass Ξ± Ξ² (f i)], VAddAssocClass Ξ± Ξ² ((i : I) β†’ f i)
Pi.vaddAssocClass
@[to_additive
Pi.vaddAssocClass': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {Ξ± : Type u_2} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : (i : I) β†’ VAdd (f i) (g i)] [inst_2 : (i : I) β†’ VAdd Ξ± (g i)] [inst_3 : βˆ€ (i : I), VAddAssocClass Ξ± (f i) (g i)], VAddAssocClass Ξ± ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.vaddAssocClass'
] instance
isScalarTower': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {Ξ± : Type u_2} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : (i : I) β†’ SMul (f i) (g i)] [inst_2 : (i : I) β†’ SMul Ξ± (g i)] [inst_3 : βˆ€ (i : I), IsScalarTower Ξ± (f i) (g i)], IsScalarTower Ξ± ((i : I) β†’ f i) ((i : I) β†’ g i)
isScalarTower'
{
g: I β†’ Type ?u.1475
g
:
I: Type u
I
β†’
Type _: Type (?u.1475+1)
Type _
} {
Ξ±: Type ?u.1478
Ξ±
:
Type _: Type (?u.1478+1)
Type _
} [βˆ€
i: ?m.1482
i
,
SMul: Type ?u.1486 β†’ Type ?u.1485 β†’ Type (max?u.1486?u.1485)
SMul
Ξ±: Type ?u.1478
Ξ±
<|
f: I β†’ Type v
f
i: ?m.1482
i
] [βˆ€
i: ?m.1491
i
,
SMul: Type ?u.1495 β†’ Type ?u.1494 β†’ Type (max?u.1495?u.1494)
SMul
(
f: I β†’ Type v
f
i: ?m.1491
i
) (
g: I β†’ Type ?u.1475
g
i: ?m.1491
i
)] [βˆ€
i: ?m.1500
i
,
SMul: Type ?u.1504 β†’ Type ?u.1503 β†’ Type (max?u.1504?u.1503)
SMul
Ξ±: Type ?u.1478
Ξ±
<|
g: I β†’ Type ?u.1475
g
i: ?m.1500
i
] [βˆ€
i: ?m.1509
i
,
IsScalarTower: (M : Type ?u.1514) β†’ (N : Type ?u.1513) β†’ (Ξ± : Type ?u.1512) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower
Ξ±: Type ?u.1478
Ξ±
(
f: I β†’ Type v
f
i: ?m.1509
i
) (
g: I β†’ Type ?u.1475
g
i: ?m.1509
i
)] :
IsScalarTower: (M : Type ?u.1570) β†’ (N : Type ?u.1569) β†’ (Ξ± : Type ?u.1568) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower
Ξ±: Type ?u.1478
Ξ±
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
) (βˆ€
i: I
i
:
I: Type u
I
,
g: I β†’ Type ?u.1475
g
i: I
i
) := ⟨fun
x: ?m.1848
x
y: ?m.1851
y
z: ?m.1854
z
=>
funext: βˆ€ {Ξ± : Sort ?u.1858} {Ξ² : Ξ± β†’ Sort ?u.1857} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
i: ?m.1872
i
=>
smul_assoc: βˆ€ {Ξ± : Type ?u.1876} {M : Type ?u.1874} {N : Type ?u.1875} [inst : SMul M N] [inst_1 : SMul N Ξ±] [inst_2 : SMul M Ξ±] [inst_3 : IsScalarTower M N Ξ±] (x : M) (y : N) (z : Ξ±), (x β€’ y) β€’ z = x β€’ y β€’ z
smul_assoc
x: ?m.1848
x
(
y: ?m.1851
y
i: ?m.1872
i
) (
z: ?m.1854
z
i: ?m.1872
i
)⟩ #align pi.is_scalar_tower'
Pi.isScalarTower': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {Ξ± : Type u_2} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : (i : I) β†’ SMul (f i) (g i)] [inst_2 : (i : I) β†’ SMul Ξ± (g i)] [inst_3 : βˆ€ (i : I), IsScalarTower Ξ± (f i) (g i)], IsScalarTower Ξ± ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.isScalarTower'
#align pi.vadd_assoc_class'
Pi.vaddAssocClass': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {Ξ± : Type u_2} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : (i : I) β†’ VAdd (f i) (g i)] [inst_2 : (i : I) β†’ VAdd Ξ± (g i)] [inst_3 : βˆ€ (i : I), VAddAssocClass Ξ± (f i) (g i)], VAddAssocClass Ξ± ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.vaddAssocClass'
@[to_additive
Pi.vaddAssocClass'': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {h : I β†’ Type u_2} [inst : (i : I) β†’ VAdd (f i) (g i)] [inst_1 : (i : I) β†’ VAdd (g i) (h i)] [inst_2 : (i : I) β†’ VAdd (f i) (h i)] [inst_3 : βˆ€ (i : I), VAddAssocClass (f i) (g i) (h i)], VAddAssocClass ((i : I) β†’ f i) ((i : I) β†’ g i) ((i : I) β†’ h i)
Pi.vaddAssocClass''
] instance
isScalarTower'': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {h : I β†’ Type u_2} [inst : (i : I) β†’ SMul (f i) (g i)] [inst_1 : (i : I) β†’ SMul (g i) (h i)] [inst_2 : (i : I) β†’ SMul (f i) (h i)] [inst_3 : βˆ€ (i : I), IsScalarTower (f i) (g i) (h i)], IsScalarTower ((i : I) β†’ f i) ((i : I) β†’ g i) ((i : I) β†’ h i)
isScalarTower''
{
g: I β†’ Type ?u.2363
g
:
I: Type u
I
β†’
Type _: Type (?u.2363+1)
Type _
} {
h: I β†’ Type ?u.2368
h
:
I: Type u
I
β†’
Type _: Type (?u.2368+1)
Type _
} [βˆ€
i: ?m.2372
i
,
SMul: Type ?u.2376 β†’ Type ?u.2375 β†’ Type (max?u.2376?u.2375)
SMul
(
f: I β†’ Type v
f
i: ?m.2372
i
) (
g: I β†’ Type ?u.2363
g
i: ?m.2372
i
)] [βˆ€
i: ?m.2381
i
,
SMul: Type ?u.2385 β†’ Type ?u.2384 β†’ Type (max?u.2385?u.2384)
SMul
(
g: I β†’ Type ?u.2363
g
i: ?m.2381
i
) (
h: I β†’ Type ?u.2368
h
i: ?m.2381
i
)] [βˆ€
i: ?m.2390
i
,
SMul: Type ?u.2394 β†’ Type ?u.2393 β†’ Type (max?u.2394?u.2393)
SMul
(
f: I β†’ Type v
f
i: ?m.2390
i
) (
h: I β†’ Type ?u.2368
h
i: ?m.2390
i
)] [βˆ€
i: ?m.2399
i
,
IsScalarTower: (M : Type ?u.2404) β†’ (N : Type ?u.2403) β†’ (Ξ± : Type ?u.2402) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower
(
f: I β†’ Type v
f
i: ?m.2399
i
) (
g: I β†’ Type ?u.2363
g
i: ?m.2399
i
) (
h: I β†’ Type ?u.2368
h
i: ?m.2399
i
)] :
IsScalarTower: (M : Type ?u.2461) β†’ (N : Type ?u.2460) β†’ (Ξ± : Type ?u.2459) β†’ [inst : SMul M N] β†’ [inst : SMul N Ξ±] β†’ [inst : SMul M Ξ±] β†’ Prop
IsScalarTower
(βˆ€
i: ?m.2463
i
,
f: I β†’ Type v
f
i: ?m.2463
i
) (βˆ€
i: ?m.2468
i
,
g: I β†’ Type ?u.2363
g
i: ?m.2468
i
) (βˆ€
i: ?m.2473
i
,
h: I β†’ Type ?u.2368
h
i: ?m.2473
i
) := ⟨fun
x: ?m.2765
x
y: ?m.2768
y
z: ?m.2772
z
=>
funext: βˆ€ {Ξ± : Sort ?u.2776} {Ξ² : Ξ± β†’ Sort ?u.2775} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
i: ?m.2790
i
=>
smul_assoc: βˆ€ {Ξ± : Type ?u.2794} {M : Type ?u.2792} {N : Type ?u.2793} [inst : SMul M N] [inst_1 : SMul N Ξ±] [inst_2 : SMul M Ξ±] [inst_3 : IsScalarTower M N Ξ±] (x : M) (y : N) (z : Ξ±), (x β€’ y) β€’ z = x β€’ y β€’ z
smul_assoc
(
x: ?m.2765
x
i: ?m.2790
i
) (
y: ?m.2768
y
i: ?m.2790
i
) (
z: ?m.2772
z
i: ?m.2790
i
)⟩ #align pi.is_scalar_tower''
Pi.isScalarTower'': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {h : I β†’ Type u_2} [inst : (i : I) β†’ SMul (f i) (g i)] [inst_1 : (i : I) β†’ SMul (g i) (h i)] [inst_2 : (i : I) β†’ SMul (f i) (h i)] [inst_3 : βˆ€ (i : I), IsScalarTower (f i) (g i) (h i)], IsScalarTower ((i : I) β†’ f i) ((i : I) β†’ g i) ((i : I) β†’ h i)
Pi.isScalarTower''
#align pi.vadd_assoc_class''
Pi.vaddAssocClass'': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {h : I β†’ Type u_2} [inst : (i : I) β†’ VAdd (f i) (g i)] [inst_1 : (i : I) β†’ VAdd (g i) (h i)] [inst_2 : (i : I) β†’ VAdd (f i) (h i)] [inst_3 : βˆ€ (i : I), VAddAssocClass (f i) (g i) (h i)], VAddAssocClass ((i : I) β†’ f i) ((i : I) β†’ g i) ((i : I) β†’ h i)
Pi.vaddAssocClass''
@[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : (i : I) β†’ VAdd Ξ² (f i)] [inst_2 : βˆ€ (i : I), VAddCommClass Ξ± Ξ² (f i)], VAddCommClass Ξ± Ξ² ((i : I) β†’ f i)
to_additive
] instance
smulCommClass: βˆ€ {Ξ± : Type ?u.3310} {Ξ² : Type ?u.3313} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : (i : I) β†’ SMul Ξ² (f i)] [inst_2 : βˆ€ (i : I), SMulCommClass Ξ± Ξ² (f i)], SMulCommClass Ξ± Ξ² ((i : I) β†’ f i)
smulCommClass
{
Ξ±: Type ?u.3310
Ξ±
Ξ²: Type ?u.3313
Ξ²
:
Type _: Type (?u.3313+1)
Type _
} [βˆ€
i: ?m.3317
i
,
SMul: Type ?u.3321 β†’ Type ?u.3320 β†’ Type (max?u.3321?u.3320)
SMul
Ξ±: Type ?u.3310
Ξ±
<|
f: I β†’ Type v
f
i: ?m.3317
i
] [βˆ€
i: ?m.3326
i
,
SMul: Type ?u.3330 β†’ Type ?u.3329 β†’ Type (max?u.3330?u.3329)
SMul
Ξ²: Type ?u.3313
Ξ²
<|
f: I β†’ Type v
f
i: ?m.3326
i
] [βˆ€
i: ?m.3335
i
,
SMulCommClass: (M : Type ?u.3340) β†’ (N : Type ?u.3339) β†’ (Ξ± : Type ?u.3338) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul N Ξ±] β†’ Prop
SMulCommClass
Ξ±: Type ?u.3310
Ξ±
Ξ²: Type ?u.3313
Ξ²
(
f: I β†’ Type v
f
i: ?m.3335
i
)] :
SMulCommClass: (M : Type ?u.3376) β†’ (N : Type ?u.3375) β†’ (Ξ± : Type ?u.3374) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul N Ξ±] β†’ Prop
SMulCommClass
Ξ±: Type ?u.3310
Ξ±
Ξ²: Type ?u.3313
Ξ²
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
) := ⟨fun
x: ?m.3548
x
y: ?m.3551
y
z: ?m.3554
z
=>
funext: βˆ€ {Ξ± : Sort ?u.3557} {Ξ² : Ξ± β†’ Sort ?u.3556} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
i: ?m.3571
i
=>
smul_comm: βˆ€ {M : Type ?u.3575} {N : Type ?u.3574} {Ξ± : Type ?u.3573} [inst : SMul M Ξ±] [inst_1 : SMul N Ξ±] [self : SMulCommClass M N Ξ±] (m : M) (n : N) (a : Ξ±), m β€’ n β€’ a = n β€’ m β€’ a
smul_comm
x: ?m.3548
x
y: ?m.3551
y
(
z: ?m.3554
z
i: ?m.3571
i
)⟩ #align pi.smul_comm_class
Pi.smulCommClass: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : (i : I) β†’ SMul Ξ² (f i)] [inst_2 : βˆ€ (i : I), SMulCommClass Ξ± Ξ² (f i)], SMulCommClass Ξ± Ξ² ((i : I) β†’ f i)
Pi.smulCommClass
#align pi.vadd_comm_class
Pi.vaddCommClass: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : (i : I) β†’ VAdd Ξ² (f i)] [inst_2 : βˆ€ (i : I), VAddCommClass Ξ± Ξ² (f i)], VAddCommClass Ξ± Ξ² ((i : I) β†’ f i)
Pi.vaddCommClass
@[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {Ξ± : Type u_2} [inst : (i : I) β†’ VAdd Ξ± (g i)] [inst_1 : (i : I) β†’ VAdd (f i) (g i)] [inst_2 : βˆ€ (i : I), VAddCommClass Ξ± (f i) (g i)], VAddCommClass Ξ± ((i : I) β†’ f i) ((i : I) β†’ g i)
to_additive
] instance
smulCommClass': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {Ξ± : Type u_2} [inst : (i : I) β†’ SMul Ξ± (g i)] [inst_1 : (i : I) β†’ SMul (f i) (g i)] [inst_2 : βˆ€ (i : I), SMulCommClass Ξ± (f i) (g i)], SMulCommClass Ξ± ((i : I) β†’ f i) ((i : I) β†’ g i)
smulCommClass'
{
g: I β†’ Type ?u.3926
g
:
I: Type u
I
β†’
Type _: Type (?u.3926+1)
Type _
} {
Ξ±: Type ?u.3929
Ξ±
:
Type _: Type (?u.3929+1)
Type _
} [βˆ€
i: ?m.3933
i
,
SMul: Type ?u.3937 β†’ Type ?u.3936 β†’ Type (max?u.3937?u.3936)
SMul
Ξ±: Type ?u.3929
Ξ±
<|
g: I β†’ Type ?u.3926
g
i: ?m.3933
i
] [βˆ€
i: ?m.3942
i
,
SMul: Type ?u.3946 β†’ Type ?u.3945 β†’ Type (max?u.3946?u.3945)
SMul
(
f: I β†’ Type v
f
i: ?m.3942
i
) (
g: I β†’ Type ?u.3926
g
i: ?m.3942
i
)] [βˆ€
i: ?m.3951
i
,
SMulCommClass: (M : Type ?u.3956) β†’ (N : Type ?u.3955) β†’ (Ξ± : Type ?u.3954) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul N Ξ±] β†’ Prop
SMulCommClass
Ξ±: Type ?u.3929
Ξ±
(
f: I β†’ Type v
f
i: ?m.3951
i
) (
g: I β†’ Type ?u.3926
g
i: ?m.3951
i
)] :
SMulCommClass: (M : Type ?u.3993) β†’ (N : Type ?u.3992) β†’ (Ξ± : Type ?u.3991) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul N Ξ±] β†’ Prop
SMulCommClass
Ξ±: Type ?u.3929
Ξ±
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
) (βˆ€
i: I
i
:
I: Type u
I
,
g: I β†’ Type ?u.3926
g
i: I
i
) := ⟨fun
x: ?m.4182
x
y: ?m.4185
y
z: ?m.4188
z
=>
funext: βˆ€ {Ξ± : Sort ?u.4192} {Ξ² : Ξ± β†’ Sort ?u.4191} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
i: ?m.4206
i
=>
smul_comm: βˆ€ {M : Type ?u.4210} {N : Type ?u.4209} {Ξ± : Type ?u.4208} [inst : SMul M Ξ±] [inst_1 : SMul N Ξ±] [self : SMulCommClass M N Ξ±] (m : M) (n : N) (a : Ξ±), m β€’ n β€’ a = n β€’ m β€’ a
smul_comm
x: ?m.4182
x
(
y: ?m.4185
y
i: ?m.4206
i
) (
z: ?m.4188
z
i: ?m.4206
i
)⟩ #align pi.smul_comm_class'
Pi.smulCommClass': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {Ξ± : Type u_2} [inst : (i : I) β†’ SMul Ξ± (g i)] [inst_1 : (i : I) β†’ SMul (f i) (g i)] [inst_2 : βˆ€ (i : I), SMulCommClass Ξ± (f i) (g i)], SMulCommClass Ξ± ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.smulCommClass'
#align pi.vadd_comm_class'
Pi.vaddCommClass': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {Ξ± : Type u_2} [inst : (i : I) β†’ VAdd Ξ± (g i)] [inst_1 : (i : I) β†’ VAdd (f i) (g i)] [inst_2 : βˆ€ (i : I), VAddCommClass Ξ± (f i) (g i)], VAddCommClass Ξ± ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.vaddCommClass'
@[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {h : I β†’ Type u_2} [inst : (i : I) β†’ VAdd (g i) (h i)] [inst_1 : (i : I) β†’ VAdd (f i) (h i)] [inst_2 : βˆ€ (i : I), VAddCommClass (f i) (g i) (h i)], VAddCommClass ((i : I) β†’ f i) ((i : I) β†’ g i) ((i : I) β†’ h i)
to_additive
] instance
smulCommClass'': βˆ€ {g : I β†’ Type ?u.4586} {h : I β†’ Type ?u.4591} [inst : (i : I) β†’ SMul (g i) (h i)] [inst_1 : (i : I) β†’ SMul (f i) (h i)] [inst_2 : βˆ€ (i : I), SMulCommClass (f i) (g i) (h i)], SMulCommClass ((i : I) β†’ f i) ((i : I) β†’ g i) ((i : I) β†’ h i)
smulCommClass''
{
g: I β†’ Type ?u.4586
g
:
I: Type u
I
β†’
Type _: Type (?u.4586+1)
Type _
} {
h: I β†’ Type ?u.4591
h
:
I: Type u
I
β†’
Type _: Type (?u.4591+1)
Type _
} [βˆ€
i: ?m.4595
i
,
SMul: Type ?u.4599 β†’ Type ?u.4598 β†’ Type (max?u.4599?u.4598)
SMul
(
g: I β†’ Type ?u.4586
g
i: ?m.4595
i
) (
h: I β†’ Type ?u.4591
h
i: ?m.4595
i
)] [βˆ€
i: ?m.4604
i
,
SMul: Type ?u.4608 β†’ Type ?u.4607 β†’ Type (max?u.4608?u.4607)
SMul
(
f: I β†’ Type v
f
i: ?m.4604
i
) (
h: I β†’ Type ?u.4591
h
i: ?m.4604
i
)] [βˆ€
i: ?m.4613
i
,
SMulCommClass: (M : Type ?u.4618) β†’ (N : Type ?u.4617) β†’ (Ξ± : Type ?u.4616) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul N Ξ±] β†’ Prop
SMulCommClass
(
f: I β†’ Type v
f
i: ?m.4613
i
) (
g: I β†’ Type ?u.4586
g
i: ?m.4613
i
) (
h: I β†’ Type ?u.4591
h
i: ?m.4613
i
)] :
SMulCommClass: (M : Type ?u.4656) β†’ (N : Type ?u.4655) β†’ (Ξ± : Type ?u.4654) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul N Ξ±] β†’ Prop
SMulCommClass
(βˆ€
i: ?m.4658
i
,
f: I β†’ Type v
f
i: ?m.4658
i
) (βˆ€
i: ?m.4663
i
,
g: I β†’ Type ?u.4586
g
i: ?m.4663
i
) (βˆ€
i: ?m.4668
i
,
h: I β†’ Type ?u.4591
h
i: ?m.4668
i
) := ⟨fun
x: ?m.4863
x
y: ?m.4866
y
z: ?m.4870
z
=>
funext: βˆ€ {Ξ± : Sort ?u.4874} {Ξ² : Ξ± β†’ Sort ?u.4873} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
i: ?m.4888
i
=>
smul_comm: βˆ€ {M : Type ?u.4892} {N : Type ?u.4891} {Ξ± : Type ?u.4890} [inst : SMul M Ξ±] [inst_1 : SMul N Ξ±] [self : SMulCommClass M N Ξ±] (m : M) (n : N) (a : Ξ±), m β€’ n β€’ a = n β€’ m β€’ a
smul_comm
(
x: ?m.4863
x
i: ?m.4888
i
) (
y: ?m.4866
y
i: ?m.4888
i
) (
z: ?m.4870
z
i: ?m.4888
i
)⟩ #align pi.smul_comm_class''
Pi.smulCommClass'': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {h : I β†’ Type u_2} [inst : (i : I) β†’ SMul (g i) (h i)] [inst_1 : (i : I) β†’ SMul (f i) (h i)] [inst_2 : βˆ€ (i : I), SMulCommClass (f i) (g i) (h i)], SMulCommClass ((i : I) β†’ f i) ((i : I) β†’ g i) ((i : I) β†’ h i)
Pi.smulCommClass''
#align pi.vadd_comm_class''
Pi.vaddCommClass'': βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} {h : I β†’ Type u_2} [inst : (i : I) β†’ VAdd (g i) (h i)] [inst_1 : (i : I) β†’ VAdd (f i) (h i)] [inst_2 : βˆ€ (i : I), VAddCommClass (f i) (g i) (h i)], VAddCommClass ((i : I) β†’ f i) ((i : I) β†’ g i) ((i : I) β†’ h i)
Pi.vaddCommClass''
@[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : (i : I) β†’ VAdd αᡃᡒᡖ (f i)] [inst_2 : βˆ€ (i : I), IsCentralVAdd Ξ± (f i)], IsCentralVAdd Ξ± ((i : I) β†’ f i)
to_additive
] instance
isCentralScalar: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : (i : I) β†’ SMul αᡐᡒᡖ (f i)] [inst_2 : βˆ€ (i : I), IsCentralScalar Ξ± (f i)], IsCentralScalar Ξ± ((i : I) β†’ f i)
isCentralScalar
{
Ξ±: Type ?u.5289
Ξ±
:
Type _: Type (?u.5289+1)
Type _
} [βˆ€
i: ?m.5293
i
,
SMul: Type ?u.5297 β†’ Type ?u.5296 β†’ Type (max?u.5297?u.5296)
SMul
Ξ±: Type ?u.5289
Ξ±
<|
f: I β†’ Type v
f
i: ?m.5293
i
] [βˆ€
i: ?m.5302
i
,
SMul: Type ?u.5306 β†’ Type ?u.5305 β†’ Type (max?u.5306?u.5305)
SMul
Ξ±: Type ?u.5289
Ξ±
ᡐᡒᡖ <|
f: I β†’ Type v
f
i: ?m.5302
i
] [βˆ€
i: ?m.5312
i
,
IsCentralScalar: (M : Type ?u.5316) β†’ (Ξ± : Type ?u.5315) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul Mᡐᡒᡖ Ξ±] β†’ Prop
IsCentralScalar
Ξ±: Type ?u.5289
Ξ±
(
f: I β†’ Type v
f
i: ?m.5312
i
)] :
IsCentralScalar: (M : Type ?u.5347) β†’ (Ξ± : Type ?u.5346) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul Mᡐᡒᡖ Ξ±] β†’ Prop
IsCentralScalar
Ξ±: Type ?u.5289
Ξ±
(βˆ€
i: ?m.5349
i
,
f: I β†’ Type v
f
i: ?m.5349
i
) := ⟨fun
_: ?m.5501
_
_: ?m.5504
_
=>
funext: βˆ€ {Ξ± : Sort ?u.5507} {Ξ² : Ξ± β†’ Sort ?u.5506} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.5521
_
=>
op_smul_eq_smul: βˆ€ {M : Type ?u.5524} {Ξ± : Type ?u.5523} [inst : SMul M Ξ±] [inst_1 : SMul Mᡐᡒᡖ Ξ±] [self : IsCentralScalar M Ξ±] (m : M) (a : Ξ±), MulOpposite.op m β€’ a = m β€’ a
op_smul_eq_smul
_: ?m.5525
_
_: ?m.5526
_
⟩ /-- If `f i` has a faithful scalar action for a given `i`, then so does `Π i, f i`. This is not an instance as `i` cannot be inferred. -/ @[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] (i : I) [inst_2 : FaithfulVAdd Ξ± (f i)], FaithfulVAdd Ξ± ((i : I) β†’ f i)
to_additive
"If `f i` has a faithful additive action for a given `i`, then so does `Ξ  i, f i`. This is not an instance as `i` cannot be inferred"] theorem
faithfulSMul_at: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] (i : I) [inst_2 : FaithfulSMul Ξ± (f i)], FaithfulSMul Ξ± ((i : I) β†’ f i)
faithfulSMul_at
{
Ξ±: Type u_1
Ξ±
:
Type _: Type (?u.5902+1)
Type _
} [βˆ€
i: ?m.5906
i
,
SMul: Type ?u.5910 β†’ Type ?u.5909 β†’ Type (max?u.5910?u.5909)
SMul
Ξ±: Type ?u.5902
Ξ±
<|
f: I β†’ Type v
f
i: ?m.5906
i
] [βˆ€
i: ?m.5915
i
,
Nonempty: Sort ?u.5918 β†’ Prop
Nonempty
(
f: I β†’ Type v
f
i: ?m.5915
i
)] (
i: I
i
:
I: Type u
I
) [
FaithfulSMul: (M : Type ?u.5925) β†’ (Ξ± : Type ?u.5924) β†’ [inst : SMul M Ξ±] β†’ Prop
FaithfulSMul
Ξ±: Type ?u.5902
Ξ±
(
f: I β†’ Type v
f
i: I
i
)] :
FaithfulSMul: (M : Type ?u.5943) β†’ (Ξ± : Type ?u.5942) β†’ [inst : SMul M Ξ±] β†’ Prop
FaithfulSMul
Ξ±: Type ?u.5902
Ξ±
(βˆ€
i: ?m.5945
i
,
f: I β†’ Type v
f
i: ?m.5945
i
) := ⟨fun
h: ?m.6038
h
=>
eq_of_smul_eq_smul: βˆ€ {M : Type ?u.6042} {Ξ± : Type ?u.6041} [inst : SMul M Ξ±] [self : FaithfulSMul M Ξ±] {m₁ mβ‚‚ : M}, (βˆ€ (a : Ξ±), m₁ β€’ a = mβ‚‚ β€’ a) β†’ m₁ = mβ‚‚
eq_of_smul_eq_smul
fun
a: f i
a
:
f: I β†’ Type v
f
i: I
i
=>

Goals accomplished! πŸ™
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i✝: I

Ξ±: Type u_1

inst✝²: (i : I) β†’ SMul Ξ± (f i)

inst✝¹: βˆ€ (i : I), Nonempty (f i)

i: I

inst✝: FaithfulSMul α (f i)

mβ‚βœ, mβ‚‚βœ: Ξ±

h: βˆ€ (a : (i : I) β†’ f i), mβ‚βœ β€’ a = mβ‚‚βœ β€’ a

a: f i


mβ‚βœ β€’ a = mβ‚‚βœ β€’ a
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i✝: I

Ξ±: Type u_1

inst✝²: (i : I) β†’ SMul Ξ± (f i)

inst✝¹: βˆ€ (i : I), Nonempty (f i)

i: I

inst✝: FaithfulSMul α (f i)

mβ‚βœ, mβ‚‚βœ: Ξ±

h: βˆ€ (a : (i : I) β†’ f i), mβ‚βœ β€’ a = mβ‚‚βœ β€’ a

a: f i


mβ‚βœ β€’ a = mβ‚‚βœ β€’ a
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i✝: I

Ξ±: Type u_1

inst✝²: (i : I) β†’ SMul Ξ± (f i)

inst✝¹: βˆ€ (i : I), Nonempty (f i)

i: I

inst✝: FaithfulSMul α (f i)

mβ‚βœ, mβ‚‚βœ: Ξ±

h: βˆ€ (a : (i : I) β†’ f i), mβ‚βœ β€’ a = mβ‚‚βœ β€’ a

a: f i

this: (mβ‚βœ β€’ Function.update (fun j => Classical.choice (_ : Nonempty (f j))) i a) i = (mβ‚‚βœ β€’ Function.update (fun j => Classical.choice (_ : Nonempty (f j))) i a) i


mβ‚βœ β€’ a = mβ‚‚βœ β€’ a
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i✝: I

Ξ±: Type u_1

inst✝²: (i : I) β†’ SMul Ξ± (f i)

inst✝¹: βˆ€ (i : I), Nonempty (f i)

i: I

inst✝: FaithfulSMul α (f i)

mβ‚βœ, mβ‚‚βœ: Ξ±

h: βˆ€ (a : (i : I) β†’ f i), mβ‚βœ β€’ a = mβ‚‚βœ β€’ a

a: f i


mβ‚βœ β€’ a = mβ‚‚βœ β€’ a

Goals accomplished! πŸ™
⟩ #align pi.has_faithful_smul_at
Pi.faithfulSMul_at: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] (i : I) [inst_2 : FaithfulSMul Ξ± (f i)], FaithfulSMul Ξ± ((i : I) β†’ f i)
Pi.faithfulSMul_at
#align pi.has_faithful_vadd_at
Pi.faithfulVAdd_at: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] (i : I) [inst_2 : FaithfulVAdd Ξ± (f i)], FaithfulVAdd Ξ± ((i : I) β†’ f i)
Pi.faithfulVAdd_at
@[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : Nonempty I] [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] [inst_2 : βˆ€ (i : I), FaithfulVAdd Ξ± (f i)], FaithfulVAdd Ξ± ((i : I) β†’ f i)
to_additive
] instance
faithfulSMul: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : Nonempty I] [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] [inst_2 : βˆ€ (i : I), FaithfulSMul Ξ± (f i)], FaithfulSMul Ξ± ((i : I) β†’ f i)
faithfulSMul
{
Ξ±: Type ?u.7332
Ξ±
:
Type _: Type (?u.7332+1)
Type _
} [
Nonempty: Sort ?u.7335 β†’ Prop
Nonempty
I: Type u
I
] [βˆ€
i: ?m.7339
i
,
SMul: Type ?u.7343 β†’ Type ?u.7342 β†’ Type (max?u.7343?u.7342)
SMul
Ξ±: Type ?u.7332
Ξ±
<|
f: I β†’ Type v
f
i: ?m.7339
i
] [βˆ€
i: ?m.7348
i
,
Nonempty: Sort ?u.7351 β†’ Prop
Nonempty
(
f: I β†’ Type v
f
i: ?m.7348
i
)] [βˆ€
i: ?m.7356
i
,
FaithfulSMul: (M : Type ?u.7360) β†’ (Ξ± : Type ?u.7359) β†’ [inst : SMul M Ξ±] β†’ Prop
FaithfulSMul
Ξ±: Type ?u.7332
Ξ±
(
f: I β†’ Type v
f
i: ?m.7356
i
)] :
FaithfulSMul: (M : Type ?u.7379) β†’ (Ξ± : Type ?u.7378) β†’ [inst : SMul M Ξ±] β†’ Prop
FaithfulSMul
Ξ±: Type ?u.7332
Ξ±
(βˆ€
i: ?m.7381
i
,
f: I β†’ Type v
f
i: ?m.7381
i
) := let ⟨
i: I
i
⟩ := β€ΉNonempty Iβ€Ί
faithfulSMul_at: βˆ€ {I : Type ?u.7459} {f : I β†’ Type ?u.7458} {Ξ± : Type ?u.7460} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] (i : I) [inst_2 : FaithfulSMul Ξ± (f i)], FaithfulSMul Ξ± ((i : I) β†’ f i)
faithfulSMul_at
i: I
i
#align pi.has_faithful_smul
Pi.faithfulSMul: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : Nonempty I] [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] [inst_2 : βˆ€ (i : I), FaithfulSMul Ξ± (f i)], FaithfulSMul Ξ± ((i : I) β†’ f i)
Pi.faithfulSMul
#align pi.has_faithful_vadd
Pi.faithfulVAdd: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : Nonempty I] [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : βˆ€ (i : I), Nonempty (f i)] [inst_2 : βˆ€ (i : I), FaithfulVAdd Ξ± (f i)], FaithfulVAdd Ξ± ((i : I) β†’ f i)
Pi.faithfulVAdd
@[
to_additive: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {m : AddMonoid Ξ±} β†’ [inst : (i : I) β†’ AddAction Ξ± (f i)] β†’ AddAction Ξ± ((i : I) β†’ f i)
to_additive
] instance
mulAction: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {m : Monoid Ξ±} β†’ [inst : (i : I) β†’ MulAction Ξ± (f i)] β†’ MulAction Ξ± ((i : I) β†’ f i)
mulAction
(
Ξ±: ?m.7842
Ξ±
) {
m: Monoid Ξ±
m
:
Monoid: Type ?u.7845 β†’ Type ?u.7845
Monoid
Ξ±: ?m.7842
Ξ±
} [βˆ€
i: ?m.7849
i
,
MulAction: (Ξ± : Type ?u.7853) β†’ Type ?u.7852 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.7853?u.7852)
MulAction
Ξ±: ?m.7842
Ξ±
<|
f: I β†’ Type v
f
i: ?m.7849
i
] : @
MulAction: (Ξ± : Type ?u.7866) β†’ Type ?u.7865 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.7866?u.7865)
MulAction
Ξ±: ?m.7842
Ξ±
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
)
m: Monoid Ξ±
m
where smul :=
(Β· β€’ Β·): Ξ± β†’ ((i : I) β†’ f i) β†’ (i : I) β†’ f i
(Β· β€’ Β·)
mul_smul
_: ?m.8878
_
_: ?m.8881
_
_: ?m.8884
_
:=
funext: βˆ€ {Ξ± : Sort ?u.8887} {Ξ² : Ξ± β†’ Sort ?u.8886} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.8897
_
=>
mul_smul: βˆ€ {Ξ± : Type ?u.8900} {Ξ² : Type ?u.8899} [inst : Monoid Ξ±] [self : MulAction Ξ± Ξ²] (x y : Ξ±) (b : Ξ²), (x * y) β€’ b = x β€’ y β€’ b
mul_smul
_: ?m.8901
_
_: ?m.8901
_
_: ?m.8902
_
one_smul
_: ?m.8810
_
:=
funext: βˆ€ {Ξ± : Sort ?u.8813} {Ξ² : Ξ± β†’ Sort ?u.8812} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.8827
_
=>
one_smul: βˆ€ (M : Type ?u.8830) {Ξ± : Type ?u.8829} [inst : Monoid M] [inst_1 : MulAction M Ξ±] (b : Ξ±), 1 β€’ b = b
one_smul
Ξ±: Type ?u.7845
Ξ±
_: ?m.8831
_
#align pi.mul_action
Pi.mulAction: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {m : Monoid Ξ±} β†’ [inst : (i : I) β†’ MulAction Ξ± (f i)] β†’ MulAction Ξ± ((i : I) β†’ f i)
Pi.mulAction
#align pi.add_action
Pi.addAction: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {m : AddMonoid Ξ±} β†’ [inst : (i : I) β†’ AddAction Ξ± (f i)] β†’ AddAction Ξ± ((i : I) β†’ f i)
Pi.addAction
@[
to_additive: {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {m : (i : I) β†’ AddMonoid (f i)} β†’ [inst : (i : I) β†’ AddAction (f i) (g i)] β†’ AddAction ((i : I) β†’ f i) ((i : I) β†’ g i)
to_additive
] instance
mulAction': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {m : (i : I) β†’ Monoid (f i)} β†’ [inst : (i : I) β†’ MulAction (f i) (g i)] β†’ MulAction ((i : I) β†’ f i) ((i : I) β†’ g i)
mulAction'
{
g: I β†’ Type ?u.9383
g
:
I: Type u
I
β†’
Type _: Type (?u.9383+1)
Type _
} {
m: (i : I) β†’ Monoid (f i)
m
: βˆ€
i: ?m.9387
i
,
Monoid: Type ?u.9390 β†’ Type ?u.9390
Monoid
(
f: I β†’ Type v
f
i: ?m.9387
i
)} [βˆ€
i: ?m.9394
i
,
MulAction: (Ξ± : Type ?u.9398) β†’ Type ?u.9397 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.9398?u.9397)
MulAction
(
f: I β†’ Type v
f
i: ?m.9394
i
) (
g: I β†’ Type ?u.9383
g
i: ?m.9394
i
)] : @
MulAction: (Ξ± : Type ?u.9415) β†’ Type ?u.9414 β†’ [inst : Monoid Ξ±] β†’ Type (max?u.9415?u.9414)
MulAction
(βˆ€
i: ?m.9417
i
,
f: I β†’ Type v
f
i: ?m.9417
i
) (βˆ€
i: I
i
:
I: Type u
I
,
g: I β†’ Type ?u.9383
g
i: I
i
) (@
Pi.monoid: {I : Type ?u.9426} β†’ {f : I β†’ Type ?u.9425} β†’ [inst : (i : I) β†’ Monoid (f i)] β†’ Monoid ((i : I) β†’ f i)
Pi.monoid
I: Type u
I
f: I β†’ Type v
f
m: (i : I) β†’ Monoid (f i)
m
) where smul :=
(Β· β€’ Β·): ((i : I) β†’ f i) β†’ ((i : I) β†’ g i) β†’ (i : I) β†’ g i
(Β· β€’ Β·)
mul_smul
_: ?m.10614
_
_: ?m.10617
_
_: ?m.10620
_
:=
funext: βˆ€ {Ξ± : Sort ?u.10624} {Ξ² : Ξ± β†’ Sort ?u.10623} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.10635
_
=>
mul_smul: βˆ€ {Ξ± : Type ?u.10638} {Ξ² : Type ?u.10637} [inst : Monoid Ξ±] [self : MulAction Ξ± Ξ²] (x y : Ξ±) (b : Ξ²), (x * y) β€’ b = x β€’ y β€’ b
mul_smul
_: ?m.10639
_
_: ?m.10639
_
_: ?m.10640
_
one_smul
_: ?m.10514
_
:=
funext: βˆ€ {Ξ± : Sort ?u.10518} {Ξ² : Ξ± β†’ Sort ?u.10517} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.10532
_
=>
one_smul: βˆ€ (M : Type ?u.10535) {Ξ± : Type ?u.10534} [inst : Monoid M] [inst_1 : MulAction M Ξ±] (b : Ξ±), 1 β€’ b = b
one_smul
_: Type ?u.10535
_
_: ?m.10537
_
#align pi.mul_action'
Pi.mulAction': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {m : (i : I) β†’ Monoid (f i)} β†’ [inst : (i : I) β†’ MulAction (f i) (g i)] β†’ MulAction ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.mulAction'
#align pi.add_action'
Pi.addAction': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {m : (i : I) β†’ AddMonoid (f i)} β†’ [inst : (i : I) β†’ AddAction (f i) (g i)] β†’ AddAction ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.addAction'
instance
smulZeroClass: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {n : (i : I) β†’ Zero (f i)} β†’ [inst : (i : I) β†’ SMulZeroClass Ξ± (f i)] β†’ SMulZeroClass Ξ± ((i : I) β†’ f i)
smulZeroClass
(
Ξ±: ?m.11191
Ξ±
) {
n: (i : I) β†’ Zero (f i)
n
: βˆ€
i: ?m.11195
i
,
Zero: Type ?u.11198 β†’ Type ?u.11198
Zero
<|
f: I β†’ Type v
f
i: ?m.11195
i
} [βˆ€
i: ?m.11202
i
,
SMulZeroClass: Type ?u.11206 β†’ (A : Type ?u.11205) β†’ [inst : Zero A] β†’ Type (max?u.11206?u.11205)
SMulZeroClass
Ξ±: ?m.11191
Ξ±
<|
f: I β†’ Type v
f
i: ?m.11202
i
] : @
SMulZeroClass: Type ?u.11229 β†’ (A : Type ?u.11228) β†’ [inst : Zero A] β†’ Type (max?u.11229?u.11228)
SMulZeroClass
Ξ±: ?m.11191
Ξ±
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
) (@
Pi.instZero: {I : Type ?u.11235} β†’ {f : I β†’ Type ?u.11234} β†’ [inst : (i : I) β†’ Zero (f i)] β†’ Zero ((i : I) β†’ f i)
Pi.instZero
I: Type u
I
f: I β†’ Type v
f
n: (i : I) β†’ Zero (f i)
n
) where smul_zero
_: ?m.11384
_
:=
funext: βˆ€ {Ξ± : Sort ?u.11387} {Ξ² : Ξ± β†’ Sort ?u.11386} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.11401
_
=>
smul_zero: βˆ€ {M : Type ?u.11404} {A : Type ?u.11403} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a β€’ 0 = 0
smul_zero
_: ?m.11405
_
#align pi.smul_zero_class
Pi.smulZeroClass: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {n : (i : I) β†’ Zero (f i)} β†’ [inst : (i : I) β†’ SMulZeroClass Ξ± (f i)] β†’ SMulZeroClass Ξ± ((i : I) β†’ f i)
Pi.smulZeroClass
instance
smulZeroClass': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {n : (i : I) β†’ Zero (g i)} β†’ [inst : (i : I) β†’ SMulZeroClass (f i) (g i)] β†’ SMulZeroClass ((i : I) β†’ f i) ((i : I) β†’ g i)
smulZeroClass'
{
g: I β†’ Type ?u.11626
g
:
I: Type u
I
β†’
Type _: Type (?u.11626+1)
Type _
} {
n: (i : I) β†’ Zero (g i)
n
: βˆ€
i: ?m.11630
i
,
Zero: Type ?u.11633 β†’ Type ?u.11633
Zero
<|
g: I β†’ Type ?u.11626
g
i: ?m.11630
i
} [βˆ€
i: ?m.11637
i
,
SMulZeroClass: Type ?u.11641 β†’ (A : Type ?u.11640) β†’ [inst : Zero A] β†’ Type (max?u.11641?u.11640)
SMulZeroClass
(
f: I β†’ Type v
f
i: ?m.11637
i
) (
g: I β†’ Type ?u.11626
g
i: ?m.11637
i
)] : @
SMulZeroClass: Type ?u.11664 β†’ (A : Type ?u.11663) β†’ [inst : Zero A] β†’ Type (max?u.11664?u.11663)
SMulZeroClass
(βˆ€
i: ?m.11666
i
,
f: I β†’ Type v
f
i: ?m.11666
i
) (βˆ€
i: I
i
:
I: Type u
I
,
g: I β†’ Type ?u.11626
g
i: I
i
) (@
Pi.instZero: {I : Type ?u.11675} β†’ {f : I β†’ Type ?u.11674} β†’ [inst : (i : I) β†’ Zero (f i)] β†’ Zero ((i : I) β†’ f i)
Pi.instZero
I: Type u
I
g: I β†’ Type ?u.11626
g
n: (i : I) β†’ Zero (g i)
n
) where smul_zero :=

Goals accomplished! πŸ™
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.11626

n: (i : I) β†’ Zero (g i)

inst✝: (i : I) β†’ SMulZeroClass (f i) (g i)


βˆ€ (a : (i : I) β†’ f i), a β€’ 0 = 0
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.11626

n: (i : I) β†’ Zero (g i)

inst✝: (i : I) β†’ SMulZeroClass (f i) (g i)

a✝: (i : I) β†’ f i


a✝ β€’ 0 = 0
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.11626

n: (i : I) β†’ Zero (g i)

inst✝: (i : I) β†’ SMulZeroClass (f i) (g i)

a✝: (i : I) β†’ f i


a✝ β€’ 0 = 0
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.11626

n: (i : I) β†’ Zero (g i)

inst✝: (i : I) β†’ SMulZeroClass (f i) (g i)


βˆ€ (a : (i : I) β†’ f i), a β€’ 0 = 0
I: Type u

f: I β†’ Type v

x✝, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.11626

n: (i : I) β†’ Zero (g i)

inst✝: (i : I) β†’ SMulZeroClass (f i) (g i)

a✝: (i : I) β†’ f i

x: I


h
I: Type u

f: I β†’ Type v

x✝, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.11626

n: (i : I) β†’ Zero (g i)

inst✝: (i : I) β†’ SMulZeroClass (f i) (g i)

a✝: (i : I) β†’ f i

x: I


h
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.11626

n: (i : I) β†’ Zero (g i)

inst✝: (i : I) β†’ SMulZeroClass (f i) (g i)


βˆ€ (a : (i : I) β†’ f i), a β€’ 0 = 0

Goals accomplished! πŸ™
#align pi.smul_zero_class'
Pi.smulZeroClass': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {n : (i : I) β†’ Zero (g i)} β†’ [inst : (i : I) β†’ SMulZeroClass (f i) (g i)] β†’ SMulZeroClass ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.smulZeroClass'
instance
distribSMul: (Ξ± : Type ?u.12128) β†’ {n : (i : I) β†’ AddZeroClass (f i)} β†’ [inst : (i : I) β†’ DistribSMul Ξ± (f i)] β†’ DistribSMul Ξ± ((i : I) β†’ f i)
distribSMul
(
Ξ±: ?m.12113
Ξ±
) {
n: (i : I) β†’ AddZeroClass (f i)
n
: βˆ€
i: ?m.12117
i
,
AddZeroClass: Type ?u.12120 β†’ Type ?u.12120
AddZeroClass
<|
f: I β†’ Type v
f
i: ?m.12117
i
} [βˆ€
i: ?m.12124
i
,
DistribSMul: Type ?u.12128 β†’ (A : Type ?u.12127) β†’ [inst : AddZeroClass A] β†’ Type (max?u.12128?u.12127)
DistribSMul
Ξ±: ?m.12113
Ξ±
<|
f: I β†’ Type v
f
i: ?m.12124
i
] : @
DistribSMul: Type ?u.12141 β†’ (A : Type ?u.12140) β†’ [inst : AddZeroClass A] β†’ Type (max?u.12141?u.12140)
DistribSMul
Ξ±: ?m.12113
Ξ±
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
) (@
Pi.addZeroClass: {I : Type ?u.12147} β†’ {f : I β†’ Type ?u.12146} β†’ [inst : (i : I) β†’ AddZeroClass (f i)] β†’ AddZeroClass ((i : I) β†’ f i)
Pi.addZeroClass
I: Type u
I
f: I β†’ Type v
f
n: (i : I) β†’ AddZeroClass (f i)
n
) where smul_zero
_: ?m.13696
_
:=
funext: βˆ€ {Ξ± : Sort ?u.13699} {Ξ² : Ξ± β†’ Sort ?u.13698} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.13713
_
=>
smul_zero: βˆ€ {M : Type ?u.13716} {A : Type ?u.13715} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a β€’ 0 = 0
smul_zero
_: ?m.13717
_
smul_add
_: ?m.14067
_
_: ?m.14070
_
_: ?m.14073
_
:=
funext: βˆ€ {Ξ± : Sort ?u.14076} {Ξ² : Ξ± β†’ Sort ?u.14075} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.14086
_
=>
smul_add: βˆ€ {M : Type ?u.14089} {A : Type ?u.14088} [inst : AddZeroClass A] [inst_1 : DistribSMul M A] (a : M) (b₁ bβ‚‚ : A), a β€’ (b₁ + bβ‚‚) = a β€’ b₁ + a β€’ bβ‚‚
smul_add
_: ?m.14090
_
_: ?m.14091
_
_: ?m.14091
_
#align pi.distrib_smul
Pi.distribSMul: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {n : (i : I) β†’ AddZeroClass (f i)} β†’ [inst : (i : I) β†’ DistribSMul Ξ± (f i)] β†’ DistribSMul Ξ± ((i : I) β†’ f i)
Pi.distribSMul
instance
distribSMul': {g : I β†’ Type ?u.14402} β†’ {n : (i : I) β†’ AddZeroClass (g i)} β†’ [inst : (i : I) β†’ DistribSMul (f i) (g i)] β†’ DistribSMul ((i : I) β†’ f i) ((i : I) β†’ g i)
distribSMul'
{
g: I β†’ Type ?u.14402
g
:
I: Type u
I
β†’
Type _: Type (?u.14402+1)
Type _
} {
n: (i : I) β†’ AddZeroClass (g i)
n
: βˆ€
i: ?m.14406
i
,
AddZeroClass: Type ?u.14409 β†’ Type ?u.14409
AddZeroClass
<|
g: I β†’ Type ?u.14402
g
i: ?m.14406
i
} [βˆ€
i: ?m.14413
i
,
DistribSMul: Type ?u.14417 β†’ (A : Type ?u.14416) β†’ [inst : AddZeroClass A] β†’ Type (max?u.14417?u.14416)
DistribSMul
(
f: I β†’ Type v
f
i: ?m.14413
i
) (
g: I β†’ Type ?u.14402
g
i: ?m.14413
i
)] : @
DistribSMul: Type ?u.14430 β†’ (A : Type ?u.14429) β†’ [inst : AddZeroClass A] β†’ Type (max?u.14430?u.14429)
DistribSMul
(βˆ€
i: ?m.14432
i
,
f: I β†’ Type v
f
i: ?m.14432
i
) (βˆ€
i: I
i
:
I: Type u
I
,
g: I β†’ Type ?u.14402
g
i: I
i
) (@
Pi.addZeroClass: {I : Type ?u.14441} β†’ {f : I β†’ Type ?u.14440} β†’ [inst : (i : I) β†’ AddZeroClass (f i)] β†’ AddZeroClass ((i : I) β†’ f i)
Pi.addZeroClass
I: Type u
I
g: I β†’ Type ?u.14402
g
n: (i : I) β†’ AddZeroClass (g i)
n
) where smul_zero :=

Goals accomplished! πŸ™
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)


βˆ€ (a : (i : I) β†’ f i), a β€’ 0 = 0
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)

a✝: (i : I) β†’ f i


a✝ β€’ 0 = 0
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)

a✝: (i : I) β†’ f i


a✝ β€’ 0 = 0
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)


βˆ€ (a : (i : I) β†’ f i), a β€’ 0 = 0
I: Type u

f: I β†’ Type v

x✝, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)

a✝: (i : I) β†’ f i

x: I


h
I: Type u

f: I β†’ Type v

x✝, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)

a✝: (i : I) β†’ f i

x: I


h
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)


βˆ€ (a : (i : I) β†’ f i), a β€’ 0 = 0

Goals accomplished! πŸ™
smul_add :=

Goals accomplished! πŸ™
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)


βˆ€ (a : (i : I) β†’ f i) (x y : (i : I) β†’ g i), a β€’ (x + y) = a β€’ x + a β€’ y
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)

a✝: (i : I) β†’ f i

x✝, y✝: (i : I) β†’ g i


a✝ β€’ (x✝ + y✝) = a✝ β€’ x✝ + a✝ β€’ y✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)

a✝: (i : I) β†’ f i

x✝, y✝: (i : I) β†’ g i


a✝ β€’ (x✝ + y✝) = a✝ β€’ x✝ + a✝ β€’ y✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)


βˆ€ (a : (i : I) β†’ f i) (x y : (i : I) β†’ g i), a β€’ (x + y) = a β€’ x + a β€’ y
I: Type u

f: I β†’ Type v

x✝¹, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)

a✝: (i : I) β†’ f i

x✝, y✝: (i : I) β†’ g i

x: I


h
(a✝ β€’ (x✝ + y✝)) x = (a✝ β€’ x✝ + a✝ β€’ y✝) x
I: Type u

f: I β†’ Type v

x✝¹, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)

a✝: (i : I) β†’ f i

x✝, y✝: (i : I) β†’ g i

x: I


h
(a✝ β€’ (x✝ + y✝)) x = (a✝ β€’ x✝ + a✝ β€’ y✝) x
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.14402

n: (i : I) β†’ AddZeroClass (g i)

inst✝: (i : I) β†’ DistribSMul (f i) (g i)


βˆ€ (a : (i : I) β†’ f i) (x y : (i : I) β†’ g i), a β€’ (x + y) = a β€’ x + a β€’ y

Goals accomplished! πŸ™
#align pi.distrib_smul'
Pi.distribSMul': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {n : (i : I) β†’ AddZeroClass (g i)} β†’ [inst : (i : I) β†’ DistribSMul (f i) (g i)] β†’ DistribSMul ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.distribSMul'
instance
distribMulAction: (Ξ± : Type ?u.16943) β†’ {m : Monoid Ξ±} β†’ {n : (i : I) β†’ AddMonoid (f i)} β†’ [inst : (i : I) β†’ DistribMulAction Ξ± (f i)] β†’ DistribMulAction Ξ± ((i : I) β†’ f i)
distribMulAction
(
Ξ±: Type ?u.16943
Ξ±
) {
m: Monoid Ξ±
m
:
Monoid: Type ?u.16943 β†’ Type ?u.16943
Monoid
Ξ±: ?m.16940
Ξ±
} {
n: (i : I) β†’ AddMonoid (f i)
n
: βˆ€
i: ?m.16947
i
,
AddMonoid: Type ?u.16950 β†’ Type ?u.16950
AddMonoid
<|
f: I β†’ Type v
f
i: ?m.16947
i
} [βˆ€
i: ?m.16954
i
,
DistribMulAction: (M : Type ?u.16958) β†’ (A : Type ?u.16957) β†’ [inst : Monoid M] β†’ [inst : AddMonoid A] β†’ Type (max?u.16958?u.16957)
DistribMulAction
Ξ±: ?m.16940
Ξ±
<|
f: I β†’ Type v
f
i: ?m.16954
i
] : @
DistribMulAction: (M : Type ?u.16983) β†’ (A : Type ?u.16982) β†’ [inst : Monoid M] β†’ [inst : AddMonoid A] β†’ Type (max?u.16983?u.16982)
DistribMulAction
Ξ±: ?m.16940
Ξ±
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
)
m: Monoid Ξ±
m
(@
Pi.addMonoid: {I : Type ?u.16989} β†’ {f : I β†’ Type ?u.16988} β†’ [inst : (i : I) β†’ AddMonoid (f i)] β†’ AddMonoid ((i : I) β†’ f i)
Pi.addMonoid
I: Type u
I
f: I β†’ Type v
f
n: (i : I) β†’ AddMonoid (f i)
n
) :=
{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
{
Pi.mulAction: {I : Type ?u.17007} β†’ {f : I β†’ Type ?u.17006} β†’ (Ξ± : Type ?u.17005) β†’ {m : Monoid Ξ±} β†’ [inst : (i : I) β†’ MulAction Ξ± (f i)] β†’ MulAction Ξ± ((i : I) β†’ f i)
Pi.mulAction
{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
_: Type ?u.17005
_
{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
,
Pi.distribSMul: {I : Type ?u.17067} β†’ {f : I β†’ Type ?u.17066} β†’ (Ξ± : Type ?u.17065) β†’ {n : (i : I) β†’ AddZeroClass (f i)} β†’ [inst : (i : I) β†’ DistribSMul Ξ± (f i)] β†’ DistribSMul Ξ± ((i : I) β†’ f i)
Pi.distribSMul
{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
_: Type ?u.17065
_
{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
with
{ Pi.mulAction _, Pi.distribSMul _ with }: DistribMulAction ?m.17115 ?m.17116
}
#align pi.distrib_mul_action
Pi.distribMulAction: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {m : Monoid Ξ±} β†’ {n : (i : I) β†’ AddMonoid (f i)} β†’ [inst : (i : I) β†’ DistribMulAction Ξ± (f i)] β†’ DistribMulAction Ξ± ((i : I) β†’ f i)
Pi.distribMulAction
instance
distribMulAction': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {m : (i : I) β†’ Monoid (f i)} β†’ {n : (i : I) β†’ AddMonoid (g i)} β†’ [inst : (i : I) β†’ DistribMulAction (f i) (g i)] β†’ DistribMulAction ((i : I) β†’ f i) ((i : I) β†’ g i)
distribMulAction'
{
g: I β†’ Type ?u.18834
g
:
I: Type u
I
β†’
Type _: Type (?u.18834+1)
Type _
} {
m: (i : I) β†’ Monoid (f i)
m
: βˆ€
i: ?m.18838
i
,
Monoid: Type ?u.18841 β†’ Type ?u.18841
Monoid
(
f: I β†’ Type v
f
i: ?m.18838
i
)} {
n: (i : I) β†’ AddMonoid (g i)
n
: βˆ€
i: ?m.18845
i
,
AddMonoid: Type ?u.18848 β†’ Type ?u.18848
AddMonoid
<|
g: I β†’ Type ?u.18834
g
i: ?m.18845
i
} [βˆ€
i: ?m.18852
i
,
DistribMulAction: (M : Type ?u.18856) β†’ (A : Type ?u.18855) β†’ [inst : Monoid M] β†’ [inst : AddMonoid A] β†’ Type (max?u.18856?u.18855)
DistribMulAction
(
f: I β†’ Type v
f
i: ?m.18852
i
) (
g: I β†’ Type ?u.18834
g
i: ?m.18852
i
)] : @
DistribMulAction: (M : Type ?u.18885) β†’ (A : Type ?u.18884) β†’ [inst : Monoid M] β†’ [inst : AddMonoid A] β†’ Type (max?u.18885?u.18884)
DistribMulAction
(βˆ€
i: ?m.18887
i
,
f: I β†’ Type v
f
i: ?m.18887
i
) (βˆ€
i: I
i
:
I: Type u
I
,
g: I β†’ Type ?u.18834
g
i: I
i
) (@
Pi.monoid: {I : Type ?u.18896} β†’ {f : I β†’ Type ?u.18895} β†’ [inst : (i : I) β†’ Monoid (f i)] β†’ Monoid ((i : I) β†’ f i)
Pi.monoid
I: Type u
I
f: I β†’ Type v
f
m: (i : I) β†’ Monoid (f i)
m
) (@
Pi.addMonoid: {I : Type ?u.18905} β†’ {f : I β†’ Type ?u.18904} β†’ [inst : (i : I) β†’ AddMonoid (f i)] β†’ AddMonoid ((i : I) β†’ f i)
Pi.addMonoid
I: Type u
I
g: I β†’ Type ?u.18834
g
n: (i : I) β†’ AddMonoid (g i)
n
) :=
{ Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
{
Pi.mulAction': {I : Type ?u.18924} β†’ {f : I β†’ Type ?u.18923} β†’ {g : I β†’ Type ?u.18922} β†’ {m : (i : I) β†’ Monoid (f i)} β†’ [inst : (i : I) β†’ MulAction (f i) (g i)] β†’ MulAction ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.mulAction'
{ Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
,
Pi.distribSMul': {I : Type ?u.18984} β†’ {f : I β†’ Type ?u.18983} β†’ {g : I β†’ Type ?u.18982} β†’ {n : (i : I) β†’ AddZeroClass (g i)} β†’ [inst : (i : I) β†’ DistribSMul (f i) (g i)] β†’ DistribSMul ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.distribSMul'
{ Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
{ Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
with
{ Pi.mulAction', Pi.distribSMul' with }: DistribMulAction ?m.19032 ?m.19033
}
#align pi.distrib_mul_action'
Pi.distribMulAction': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {m : (i : I) β†’ Monoid (f i)} β†’ {n : (i : I) β†’ AddMonoid (g i)} β†’ [inst : (i : I) β†’ DistribMulAction (f i) (g i)] β†’ DistribMulAction ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.distribMulAction'
theorem
single_smul: βˆ€ {Ξ± : Type u_1} [inst : Monoid Ξ±] [inst_1 : (i : I) β†’ AddMonoid (f i)] [inst_2 : (i : I) β†’ DistribMulAction Ξ± (f i)] [inst_3 : DecidableEq I] (i : I) (r : Ξ±) (x : f i), single i (r β€’ x) = r β€’ single i x
single_smul
{
Ξ±: ?m.21046
Ξ±
} [
Monoid: Type ?u.21049 β†’ Type ?u.21049
Monoid
Ξ±: ?m.21046
Ξ±
] [βˆ€
i: ?m.21053
i
,
AddMonoid: Type ?u.21056 β†’ Type ?u.21056
AddMonoid
<|
f: I β†’ Type v
f
i: ?m.21053
i
] [βˆ€
i: ?m.21061
i
,
DistribMulAction: (M : Type ?u.21065) β†’ (A : Type ?u.21064) β†’ [inst : Monoid M] β†’ [inst : AddMonoid A] β†’ Type (max?u.21065?u.21064)
DistribMulAction
Ξ±: ?m.21046
Ξ±
<|
f: I β†’ Type v
f
i: ?m.21061
i
] [
DecidableEq: Sort ?u.21089 β†’ Sort (max1?u.21089)
DecidableEq
I: Type u
I
] (
i: I
i
:
I: Type u
I
) (
r: Ξ±
r
:
Ξ±: ?m.21046
Ξ±
) (
x: f i
x
:
f: I β†’ Type v
f
i: I
i
) :
single: {I : Type ?u.21106} β†’ {f : I β†’ Type ?u.21105} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
single
i: I
i
(
r: Ξ±
r
β€’
x: f i
x
) =
r: Ξ±
r
β€’
single: {I : Type ?u.22058} β†’ {f : I β†’ Type ?u.22057} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
single
i: I
i
x: f i
x
:=
single_op: βˆ€ {I : Type ?u.22853} {f : I β†’ Type ?u.22852} [inst : DecidableEq I] [inst_1 : (i : I) β†’ Zero (f i)] {g : I β†’ Type ?u.22854} [inst_2 : (i : I) β†’ Zero (g i)] (op : (i : I) β†’ f i β†’ g i), (βˆ€ (i : I), op i 0 = 0) β†’ βˆ€ (i : I) (x : f i), single i (op i x) = fun j => op j (single i x j)
single_op
(fun
i: I
i
:
I: Type u
I
=> (
(Β· β€’ Β·): Ξ± β†’ f i β†’ f i
(Β· β€’ Β·)
r: Ξ±
r
:
f: I β†’ Type v
f
i: I
i
β†’
f: I β†’ Type v
f
i: I
i
)) (fun
_: ?m.23004
_
=>
smul_zero: βˆ€ {M : Type ?u.23007} {A : Type ?u.23006} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a β€’ 0 = 0
smul_zero
_: ?m.23008
_
)
_: ?m.22855
_
_: ?m.22856 ?m.24592
_
#align pi.single_smul
Pi.single_smul: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : Monoid Ξ±] [inst_1 : (i : I) β†’ AddMonoid (f i)] [inst_2 : (i : I) β†’ DistribMulAction Ξ± (f i)] [inst_3 : DecidableEq I] (i : I) (r : Ξ±) (x : f i), single i (r β€’ x) = r β€’ single i x
Pi.single_smul
-- Porting note: Lean4 cannot infer the non-dependent function `f := fun _ => Ξ²` /-- A version of `Pi.single_smul` for non-dependent functions. It is useful in cases where Lean fails to apply `Pi.single_smul`. -/ theorem
single_smul': βˆ€ {I : Type u} {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Monoid Ξ±] [inst_1 : AddMonoid Ξ²] [inst_2 : DistribMulAction Ξ± Ξ²] [inst_3 : DecidableEq I] (i : I) (r : Ξ±) (x : Ξ²), single i (r β€’ x) = r β€’ single i x
single_smul'
{
Ξ±: Type u_1
Ξ±
Ξ²: ?m.24970
Ξ²
} [
Monoid: Type ?u.24973 β†’ Type ?u.24973
Monoid
Ξ±: ?m.24967
Ξ±
] [
AddMonoid: Type ?u.24976 β†’ Type ?u.24976
AddMonoid
Ξ²: ?m.24970
Ξ²
] [
DistribMulAction: (M : Type ?u.24980) β†’ (A : Type ?u.24979) β†’ [inst : Monoid M] β†’ [inst : AddMonoid A] β†’ Type (max?u.24980?u.24979)
DistribMulAction
Ξ±: ?m.24967
Ξ±
Ξ²: ?m.24970
Ξ²
] [
DecidableEq: Sort ?u.24999 β†’ Sort (max1?u.24999)
DecidableEq
I: Type u
I
] (
i: I
i
:
I: Type u
I
) (
r: Ξ±
r
:
Ξ±: ?m.24967
Ξ±
) (
x: Ξ²
x
:
Ξ²: ?m.24970
Ξ²
) :
single: {I : Type ?u.25016} β†’ {f : I β†’ Type ?u.25015} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
single
(f := fun
_: ?m.25019
_
=>
Ξ²: ?m.24970
Ξ²
)
i: I
i
(
r: Ξ±
r
β€’
x: Ξ²
x
) =
r: Ξ±
r
β€’
single: {I : Type ?u.26100} β†’ {f : I β†’ Type ?u.26099} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
single
(f := fun
_: ?m.26103
_
=>
Ξ²: ?m.24970
Ξ²
)
i: I
i
x: Ξ²
x
:=
single_smul: βˆ€ {I : Type ?u.27689} {f : I β†’ Type ?u.27688} {Ξ± : Type ?u.27690} [inst : Monoid Ξ±] [inst_1 : (i : I) β†’ AddMonoid (f i)] [inst_2 : (i : I) β†’ DistribMulAction Ξ± (f i)] [inst_3 : DecidableEq I] (i : I) (r : Ξ±) (x : f i), single i (r β€’ x) = r β€’ single i x
single_smul
(f := fun
_: ?m.27693
_
=>
Ξ²: Type u_2
Ξ²
)
i: I
i
r: Ξ±
r
x: Ξ²
x
#align pi.single_smul'
Pi.single_smul': βˆ€ {I : Type u} {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Monoid Ξ±] [inst_1 : AddMonoid Ξ²] [inst_2 : DistribMulAction Ξ± Ξ²] [inst_3 : DecidableEq I] (i : I) (r : Ξ±) (x : Ξ²), single i (r β€’ x) = r β€’ single i x
Pi.single_smul'
theorem
single_smulβ‚€: βˆ€ {g : I β†’ Type u_1} [inst : (i : I) β†’ MonoidWithZero (f i)] [inst_1 : (i : I) β†’ AddMonoid (g i)] [inst_2 : (i : I) β†’ DistribMulAction (f i) (g i)] [inst_3 : DecidableEq I] (i : I) (r : f i) (x : g i), single i (r β€’ x) = single i r β€’ single i x
single_smulβ‚€
{
g: I β†’ Type ?u.27847
g
:
I: Type u
I
β†’
Type _: Type (?u.27847+1)
Type _
} [βˆ€
i: ?m.27851
i
,
MonoidWithZero: Type ?u.27854 β†’ Type ?u.27854
MonoidWithZero
(
f: I β†’ Type v
f
i: ?m.27851
i
)] [βˆ€
i: ?m.27859
i
,
AddMonoid: Type ?u.27862 β†’ Type ?u.27862
AddMonoid
(
g: I β†’ Type ?u.27847
g
i: ?m.27859
i
)] [βˆ€
i: ?m.27867
i
,
DistribMulAction: (M : Type ?u.27871) β†’ (A : Type ?u.27870) β†’ [inst : Monoid M] β†’ [inst : AddMonoid A] β†’ Type (max?u.27871?u.27870)
DistribMulAction
(
f: I β†’ Type v
f
i: ?m.27867
i
) (
g: I β†’ Type ?u.27847
g
i: ?m.27867
i
)] [
DecidableEq: Sort ?u.27908 β†’ Sort (max1?u.27908)
DecidableEq
I: Type u
I
] (
i: I
i
:
I: Type u
I
) (
r: f i
r
:
f: I β†’ Type v
f
i: I
i
) (
x: g i
x
:
g: I β†’ Type ?u.27847
g
i: I
i
) :
single: {I : Type ?u.27925} β†’ {f : I β†’ Type ?u.27924} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
single
i: I
i
(
r: f i
r
β€’
x: g i
x
) =
single: {I : Type ?u.28959} β†’ {f : I β†’ Type ?u.28958} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
single
i: I
i
r: f i
r
β€’
single: {I : Type ?u.29137} β†’ {f : I β†’ Type ?u.29136} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
single
i: I
i
x: g i
x
:=
single_opβ‚‚: βˆ€ {I : Type ?u.30036} {f : I β†’ Type ?u.30035} [inst : DecidableEq I] [inst_1 : (i : I) β†’ Zero (f i)] {g₁ : I β†’ Type ?u.30037} {gβ‚‚ : I β†’ Type ?u.30038} [inst_2 : (i : I) β†’ Zero (g₁ i)] [inst_3 : (i : I) β†’ Zero (gβ‚‚ i)] (op : (i : I) β†’ g₁ i β†’ gβ‚‚ i β†’ f i), (βˆ€ (i : I), op i 0 0 = 0) β†’ βˆ€ (i : I) (x₁ : g₁ i) (xβ‚‚ : gβ‚‚ i), single i (op i x₁ xβ‚‚) = fun j => op j (single i x₁ j) (single i xβ‚‚ j)
single_opβ‚‚
(fun
i: I
i
:
I: Type u
I
=> (
(Β· β€’ Β·): f i β†’ g i β†’ g i
(Β· β€’ Β·)
:
f: I β†’ Type v
f
i: I
i
β†’
g: I β†’ Type u_1
g
i: I
i
β†’
g: I β†’ Type u_1
g
i: I
i
)) (fun
_: ?m.30458
_
=>
smul_zero: βˆ€ {M : Type ?u.30461} {A : Type ?u.30460} [inst : Zero A] [inst_1 : SMulZeroClass M A] (a : M), a β€’ 0 = 0
smul_zero
_: ?m.30462
_
)
_: ?m.30039
_
_: ?m.30043 ?m.31341
_
_: ?m.30044 ?m.31341
_
#align pi.single_smulβ‚€
Pi.single_smulβ‚€: βˆ€ {I : Type u} {f : I β†’ Type v} {g : I β†’ Type u_1} [inst : (i : I) β†’ MonoidWithZero (f i)] [inst_1 : (i : I) β†’ AddMonoid (g i)] [inst_2 : (i : I) β†’ DistribMulAction (f i) (g i)] [inst_3 : DecidableEq I] (i : I) (r : f i) (x : g i), single i (r β€’ x) = single i r β€’ single i x
Pi.single_smulβ‚€
instance
mulDistribMulAction: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {m : Monoid Ξ±} β†’ {n : (i : I) β†’ Monoid (f i)} β†’ [inst : (i : I) β†’ MulDistribMulAction Ξ± (f i)] β†’ MulDistribMulAction Ξ± ((i : I) β†’ f i)
mulDistribMulAction
(
Ξ±: Type ?u.31542
Ξ±
) {
m: Monoid Ξ±
m
:
Monoid: Type ?u.31542 β†’ Type ?u.31542
Monoid
Ξ±: ?m.31539
Ξ±
} {
n: (i : I) β†’ Monoid (f i)
n
: βˆ€
i: ?m.31546
i
,
Monoid: Type ?u.31549 β†’ Type ?u.31549
Monoid
<|
f: I β†’ Type v
f
i: ?m.31546
i
} [βˆ€
i: ?m.31553
i
,
MulDistribMulAction: (M : Type ?u.31557) β†’ (A : Type ?u.31556) β†’ [inst : Monoid M] β†’ [inst : Monoid A] β†’ Type (max?u.31557?u.31556)
MulDistribMulAction
Ξ±: ?m.31539
Ξ±
<|
f: I β†’ Type v
f
i: ?m.31553
i
] : @
MulDistribMulAction: (M : Type ?u.31585) β†’ (A : Type ?u.31584) β†’ [inst : Monoid M] β†’ [inst : Monoid A] β†’ Type (max?u.31585?u.31584)
MulDistribMulAction
Ξ±: ?m.31539
Ξ±
(βˆ€
i: I
i
:
I: Type u
I
,
f: I β†’ Type v
f
i: I
i
)
m: Monoid Ξ±
m
(@
Pi.monoid: {I : Type ?u.31591} β†’ {f : I β†’ Type ?u.31590} β†’ [inst : (i : I) β†’ Monoid (f i)] β†’ Monoid ((i : I) β†’ f i)
Pi.monoid
I: Type u
I
f: I β†’ Type v
f
n: (i : I) β†’ Monoid (f i)
n
) := {
Pi.mulAction: {I : Type ?u.31609} β†’ {f : I β†’ Type ?u.31608} β†’ (Ξ± : Type ?u.31607) β†’ {m : Monoid Ξ±} β†’ [inst : (i : I) β†’ MulAction Ξ± (f i)] β†’ MulAction Ξ± ((i : I) β†’ f i)
Pi.mulAction
_: Type ?u.31607
_
with smul_one := fun
_: ?m.31990
_
=>
funext: βˆ€ {Ξ± : Sort ?u.31993} {Ξ² : Ξ± β†’ Sort ?u.31992} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.32003
_
=>
smul_one: βˆ€ {M : Type ?u.32006} {A : Type ?u.32005} [inst : Monoid M] [inst_1 : Monoid A] [self : MulDistribMulAction M A] (r : M), r β€’ 1 = 1
smul_one
_: ?m.32007
_
smul_mul := fun
_: ?m.31793
_
_: ?m.31796
_
_: ?m.31799
_
=>
funext: βˆ€ {Ξ± : Sort ?u.31802} {Ξ² : Ξ± β†’ Sort ?u.31801} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
_: ?m.31813
_
=>
smul_mul': βˆ€ {M : Type ?u.31816} {A : Type ?u.31815} [inst : Monoid M] [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A] (a : M) (b₁ bβ‚‚ : A), a β€’ (b₁ * bβ‚‚) = a β€’ b₁ * a β€’ bβ‚‚
smul_mul'
_: ?m.31817
_
_: ?m.31818
_
_: ?m.31818
_
} #align pi.mul_distrib_mul_action
Pi.mulDistribMulAction: {I : Type u} β†’ {f : I β†’ Type v} β†’ (Ξ± : Type u_1) β†’ {m : Monoid Ξ±} β†’ {n : (i : I) β†’ Monoid (f i)} β†’ [inst : (i : I) β†’ MulDistribMulAction Ξ± (f i)] β†’ MulDistribMulAction Ξ± ((i : I) β†’ f i)
Pi.mulDistribMulAction
instance
mulDistribMulAction': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {m : (i : I) β†’ Monoid (f i)} β†’ {n : (i : I) β†’ Monoid (g i)} β†’ [inst : (i : I) β†’ MulDistribMulAction (f i) (g i)] β†’ MulDistribMulAction ((i : I) β†’ f i) ((i : I) β†’ g i)
mulDistribMulAction'
{
g: I β†’ Type ?u.32275
g
:
I: Type u
I
β†’
Type _: Type (?u.32275+1)
Type _
} {
m: (i : I) β†’ Monoid (f i)
m
: βˆ€
i: ?m.32279
i
,
Monoid: Type ?u.32282 β†’ Type ?u.32282
Monoid
(
f: I β†’ Type v
f
i: ?m.32279
i
)} {
n: (i : I) β†’ Monoid (g i)
n
: βˆ€
i: ?m.32286
i
,
Monoid: Type ?u.32289 β†’ Type ?u.32289
Monoid
<|
g: I β†’ Type ?u.32275
g
i: ?m.32286
i
} [βˆ€
i: ?m.32293
i
,
MulDistribMulAction: (M : Type ?u.32297) β†’ (A : Type ?u.32296) β†’ [inst : Monoid M] β†’ [inst : Monoid A] β†’ Type (max?u.32297?u.32296)
MulDistribMulAction
(
f: I β†’ Type v
f
i: ?m.32293
i
) (
g: I β†’ Type ?u.32275
g
i: ?m.32293
i
)] : @
MulDistribMulAction: (M : Type ?u.32329) β†’ (A : Type ?u.32328) β†’ [inst : Monoid M] β†’ [inst : Monoid A] β†’ Type (max?u.32329?u.32328)
MulDistribMulAction
(βˆ€
i: ?m.32331
i
,
f: I β†’ Type v
f
i: ?m.32331
i
) (βˆ€
i: I
i
:
I: Type u
I
,
g: I β†’ Type ?u.32275
g
i: I
i
) (@
Pi.monoid: {I : Type ?u.32340} β†’ {f : I β†’ Type ?u.32339} β†’ [inst : (i : I) β†’ Monoid (f i)] β†’ Monoid ((i : I) β†’ f i)
Pi.monoid
I: Type u
I
f: I β†’ Type v
f
m: (i : I) β†’ Monoid (f i)
m
) (@
Pi.monoid: {I : Type ?u.32349} β†’ {f : I β†’ Type ?u.32348} β†’ [inst : (i : I) β†’ Monoid (f i)] β†’ Monoid ((i : I) β†’ f i)
Pi.monoid
I: Type u
I
g: I β†’ Type ?u.32275
g
n: (i : I) β†’ Monoid (g i)
n
) where smul_mul :=

Goals accomplished! πŸ™
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)


βˆ€ (r : (i : I) β†’ f i) (x y : (i : I) β†’ g i), r β€’ (x * y) = r β€’ x * r β€’ y
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)

r✝: (i : I) β†’ f i

x✝, y✝: (i : I) β†’ g i


r✝ β€’ (x✝ * y✝) = r✝ β€’ x✝ * r✝ β€’ y✝
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)


βˆ€ (r : (i : I) β†’ f i) (x y : (i : I) β†’ g i), r β€’ (x * y) = r β€’ x * r β€’ y
I: Type u

f: I β†’ Type v

x✝¹, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)

r✝: (i : I) β†’ f i

x✝, y✝: (i : I) β†’ g i

x: I


h
(r✝ β€’ (x✝ * y✝)) x = (r✝ β€’ x✝ * r✝ β€’ y✝) x
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)


βˆ€ (r : (i : I) β†’ f i) (x y : (i : I) β†’ g i), r β€’ (x * y) = r β€’ x * r β€’ y

Goals accomplished! πŸ™
smul_one :=

Goals accomplished! πŸ™
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)


βˆ€ (r : (i : I) β†’ f i), r β€’ 1 = 1
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)

r✝: (i : I) β†’ f i


r✝ β€’ 1 = 1
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)


βˆ€ (r : (i : I) β†’ f i), r β€’ 1 = 1
I: Type u

f: I β†’ Type v

x✝, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)

r✝: (i : I) β†’ f i

x: I


h
I: Type u

f: I β†’ Type v

x, y: (i : I) β†’ f i

i: I

g: I β†’ Type ?u.32275

m: (i : I) β†’ Monoid (f i)

n: (i : I) β†’ Monoid (g i)

inst✝: (i : I) β†’ MulDistribMulAction (f i) (g i)


βˆ€ (r : (i : I) β†’ f i), r β€’ 1 = 1

Goals accomplished! πŸ™
#align pi.mul_distrib_mul_action'
Pi.mulDistribMulAction': {I : Type u} β†’ {f : I β†’ Type v} β†’ {g : I β†’ Type u_1} β†’ {m : (i : I) β†’ Monoid (f i)} β†’ {n : (i : I) β†’ Monoid (g i)} β†’ [inst : (i : I) β†’ MulDistribMulAction (f i) (g i)] β†’ MulDistribMulAction ((i : I) β†’ f i) ((i : I) β†’ g i)
Pi.mulDistribMulAction'
end Pi namespace Function /-- Non-dependent version of `Pi.smul`. Lean gets confused by the dependent instance if this is not present. -/ @[
to_additive: {ΞΉ : Type u_1} β†’ {R : Type u_2} β†’ {M : Type u_3} β†’ [inst : VAdd R M] β†’ VAdd R (ΞΉ β†’ M)
to_additive
"Non-dependent version of `Pi.vadd`. Lean gets confused by the dependent instance if this is not present."] instance
hasSMul: {ΞΉ : Type u_1} β†’ {R : Type u_2} β†’ {M : Type u_3} β†’ [inst : SMul R M] β†’ SMul R (ΞΉ β†’ M)
hasSMul
{
ΞΉ: Type ?u.32945
ΞΉ
R: Type ?u.32948
R
M: Type ?u.32951
M
:
Type _: Type (?u.32951+1)
Type _
} [
SMul: Type ?u.32955 β†’ Type ?u.32954 β†’ Type (max?u.32955?u.32954)
SMul
R: Type ?u.32948
R
M: Type ?u.32951
M
] :
SMul: Type ?u.32959 β†’ Type ?u.32958 β†’ Type (max?u.32959?u.32958)
SMul
R: Type ?u.32948
R
(
ΞΉ: Type ?u.32945
ΞΉ
β†’
M: Type ?u.32951
M
) :=
Pi.instSMul: {I : Type ?u.32971} β†’ {Ξ± : Type ?u.32969} β†’ {f : I β†’ Type ?u.32970} β†’ [inst : (i : I) β†’ SMul Ξ± (f i)] β†’ SMul Ξ± ((i : I) β†’ f i)
Pi.instSMul
#align function.has_smul
Function.hasSMul: {ΞΉ : Type u_1} β†’ {R : Type u_2} β†’ {M : Type u_3} β†’ [inst : SMul R M] β†’ SMul R (ΞΉ β†’ M)
Function.hasSMul
#align function.has_vadd
Function.hasVAdd: {ΞΉ : Type u_1} β†’ {R : Type u_2} β†’ {M : Type u_3} β†’ [inst : VAdd R M] β†’ VAdd R (ΞΉ β†’ M)
Function.hasVAdd
/-- Non-dependent version of `Pi.smulCommClass`. Lean gets confused by the dependent instance if this is not present. -/ @[
to_additive: βˆ€ {ΞΉ : Type u_1} {Ξ± : Type u_2} {Ξ² : Type u_3} {M : Type u_4} [inst : VAdd Ξ± M] [inst_1 : VAdd Ξ² M] [inst_2 : VAddCommClass Ξ± Ξ² M], VAddCommClass Ξ± Ξ² (ΞΉ β†’ M)
to_additive
"Non-dependent version of `Pi.vaddCommClass`. Lean gets confused by the dependent instance if this is not present."] instance
smulCommClass: βˆ€ {ΞΉ : Type ?u.33191} {Ξ± : Type ?u.33194} {Ξ² : Type ?u.33197} {M : Type ?u.33200} [inst : SMul Ξ± M] [inst_1 : SMul Ξ² M] [inst_2 : SMulCommClass Ξ± Ξ² M], SMulCommClass Ξ± Ξ² (ΞΉ β†’ M)
smulCommClass
{
ΞΉ: Type ?u.33191
ΞΉ
Ξ±: Type ?u.33194
Ξ±
Ξ²: Type ?u.33197
Ξ²
M: Type ?u.33200
M
:
Type _: Type (?u.33191+1)
Type _
} [
SMul: Type ?u.33204 β†’ Type ?u.33203 β†’ Type (max?u.33204?u.33203)
SMul
Ξ±: Type ?u.33194
Ξ±
M: Type ?u.33200
M
] [
SMul: Type ?u.33208 β†’ Type ?u.33207 β†’ Type (max?u.33208?u.33207)
SMul
Ξ²: Type ?u.33197
Ξ²
M: Type ?u.33200
M
] [
SMulCommClass: (M : Type ?u.33213) β†’ (N : Type ?u.33212) β†’ (Ξ± : Type ?u.33211) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul N Ξ±] β†’ Prop
SMulCommClass
Ξ±: Type ?u.33194
Ξ±
Ξ²: Type ?u.33197
Ξ²
M: Type ?u.33200
M
] :
SMulCommClass: (M : Type ?u.33240) β†’ (N : Type ?u.33239) β†’ (Ξ± : Type ?u.33238) β†’ [inst : SMul M Ξ±] β†’ [inst : SMul N Ξ±] β†’ Prop
SMulCommClass
Ξ±: Type ?u.33194
Ξ±
Ξ²: Type ?u.33197
Ξ²
(
ΞΉ: Type ?u.33191
ΞΉ
β†’
M: Type ?u.33200
M
) :=
Pi.smulCommClass: βˆ€ {I : Type ?u.33346} {f : I β†’ Type ?u.33345} {Ξ± : Type ?u.33344} {Ξ² : Type ?u.33343} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : (i : I) β†’ SMul Ξ² (f i)] [inst_2 : βˆ€ (i : I), SMulCommClass Ξ± Ξ² (f i)], SMulCommClass Ξ± Ξ² ((i : I) β†’ f i)
Pi.smulCommClass
#align function.smul_comm_class
Function.smulCommClass: βˆ€ {ΞΉ : Type u_1} {Ξ± : Type u_2} {Ξ² : Type u_3} {M : Type u_4} [inst : SMul Ξ± M] [inst_1 : SMul Ξ² M] [inst_2 : SMulCommClass Ξ± Ξ² M], SMulCommClass Ξ± Ξ² (ΞΉ β†’ M)
Function.smulCommClass
#align function.vadd_comm_class
Function.vaddCommClass: βˆ€ {ΞΉ : Type u_1} {Ξ± : Type u_2} {Ξ² : Type u_3} {M : Type u_4} [inst : VAdd Ξ± M] [inst_1 : VAdd Ξ² M] [inst_2 : VAddCommClass Ξ± Ξ² M], VAddCommClass Ξ± Ξ² (ΞΉ β†’ M)
Function.vaddCommClass
@[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : DecidableEq I] (c : Ξ±) (f₁ : (i : I) β†’ f i) (i : I) (x₁ : f i), update (c +α΅₯ f₁) i (c +α΅₯ x₁) = c +α΅₯ update f₁ i x₁
to_additive
] theorem
update_smul: βˆ€ {Ξ± : Type u_1} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : DecidableEq I] (c : Ξ±) (f₁ : (i : I) β†’ f i) (i : I) (x₁ : f i), update (c β€’ f₁) i (c β€’ x₁) = c β€’ update f₁ i x₁
update_smul
{
Ξ±: Type u_1
Ξ±
:
Type _: Type (?u.33688+1)
Type _
} [βˆ€
i: ?m.33692
i
,
SMul: Type ?u.33696 β†’ Type ?u.33695 β†’ Type (max?u.33696?u.33695)
SMul
Ξ±: Type ?u.33688
Ξ±
(
f: I β†’ Type v
f
i: ?m.33692
i
)] [
DecidableEq: Sort ?u.33700 β†’ Sort (max1?u.33700)
DecidableEq
I: Type u
I
] (
c: Ξ±
c
:
Ξ±: Type ?u.33688
Ξ±
) (
f₁: (i : I) β†’ f i
f₁
: βˆ€
i: ?m.33712
i
,
f: I β†’ Type v
f
i: ?m.33712
i
) (
i: I
i
:
I: Type u
I
) (
x₁: f i
x₁
:
f: I β†’ Type v
f
i: I
i
) :
update: {Ξ± : Sort ?u.33723} β†’ {Ξ² : Ξ± β†’ Sort ?u.33722} β†’ [inst : DecidableEq Ξ±] β†’ ((a : Ξ±) β†’ Ξ² a) β†’ (a' : Ξ±) β†’ Ξ² a' β†’ (a : Ξ±) β†’ Ξ² a
update
(
c: Ξ±
c
β€’
f₁: (i : I) β†’ f i
f₁
)
i: I
i
(
c: Ξ±
c
β€’
x₁: f i
x₁
) =
c: Ξ±
c
β€’
update: {Ξ± : Sort ?u.33882} β†’ {Ξ² : Ξ± β†’ Sort ?u.33881} β†’ [inst : DecidableEq Ξ±] β†’ ((a : Ξ±) β†’ Ξ² a) β†’ (a' : Ξ±) β†’ Ξ² a' β†’ (a : Ξ±) β†’ Ξ² a
update
f₁: (i : I) β†’ f i
f₁
i: I
i
x₁: f i
x₁
:=
funext: βˆ€ {Ξ± : Sort ?u.34010} {Ξ² : Ξ± β†’ Sort ?u.34009} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
j: ?m.34024
j
=> (
apply_update: βˆ€ {ΞΉ : Sort ?u.34026} [inst : DecidableEq ΞΉ] {Ξ± : ΞΉ β†’ Sort ?u.34027} {Ξ² : ΞΉ β†’ Sort ?u.34028} (f : (i : ΞΉ) β†’ Ξ± i β†’ Ξ² i) (g : (i : ΞΉ) β†’ Ξ± i) (i : ΞΉ) (v : Ξ± i) (j : ΞΉ), f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
apply_update
(Ξ² :=
f: I β†’ Type v
f
) (fun
_: ?m.34036
_
=>
(Β· β€’ Β·): Ξ± β†’ f x✝ β†’ f x✝
(Β· β€’ Β·)
c: Ξ±
c
)
f₁: (i : I) β†’ f i
f₁
i: I
i
x₁: f i
x₁
j: ?m.34024
j
).
symm: βˆ€ {Ξ± : Sort ?u.34207} {a b : Ξ±}, a = b β†’ b = a
symm
#align function.update_smul
Function.update_smul: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ SMul Ξ± (f i)] [inst_1 : DecidableEq I] (c : Ξ±) (f₁ : (i : I) β†’ f i) (i : I) (x₁ : f i), update (c β€’ f₁) i (c β€’ x₁) = c β€’ update f₁ i x₁
Function.update_smul
#align function.update_vadd
Function.update_vadd: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ VAdd Ξ± (f i)] [inst_1 : DecidableEq I] (c : Ξ±) (f₁ : (i : I) β†’ f i) (i : I) (x₁ : f i), update (c +α΅₯ f₁) i (c +α΅₯ x₁) = c +α΅₯ update f₁ i x₁
Function.update_vadd
end Function namespace Set @[
to_additive: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ VAdd Ξ± (f i)] (s : Set I) [inst_1 : (i : I) β†’ Decidable (i ∈ s)] (c : Ξ±) (f₁ g₁ : (i : I) β†’ f i), piecewise s (c +α΅₯ f₁) (c +α΅₯ g₁) = c +α΅₯ piecewise s f₁ g₁
to_additive
] theorem
piecewise_smul: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ SMul Ξ± (f i)] (s : Set I) [inst_1 : (i : I) β†’ Decidable (i ∈ s)] (c : Ξ±) (f₁ g₁ : (i : I) β†’ f i), piecewise s (c β€’ f₁) (c β€’ g₁) = c β€’ piecewise s f₁ g₁
piecewise_smul
{
Ξ±: Type u_1
Ξ±
:
Type _: Type (?u.34500+1)
Type _
} [βˆ€
i: ?m.34504
i
,
SMul: Type ?u.34508 β†’ Type ?u.34507 β†’ Type (max?u.34508?u.34507)
SMul
Ξ±: Type ?u.34500
Ξ±
(
f: I β†’ Type v
f
i: ?m.34504
i
)] (
s: Set I
s
:
Set: Type ?u.34512 β†’ Type ?u.34512
Set
I: Type u
I
) [βˆ€
i: ?m.34516
i
,
Decidable: Prop β†’ Type
Decidable
(
i: ?m.34516
i
∈
s: Set I
s
)] (
c: Ξ±
c
:
Ξ±: Type ?u.34500
Ξ±
) (
f₁: (i : I) β†’ f i
f₁
g₁: (i : I) β†’ f i
g₁
: βˆ€
i: ?m.34543
i
,
f: I β†’ Type v
f
i: ?m.34543
i
) :
s: Set I
s
.
piecewise: {Ξ± : Type ?u.34556} β†’ {Ξ² : Ξ± β†’ Sort ?u.34555} β†’ (s : Set Ξ±) β†’ ((i : Ξ±) β†’ Ξ² i) β†’ ((i : Ξ±) β†’ Ξ² i) β†’ [inst : (j : Ξ±) β†’ Decidable (j ∈ s)] β†’ (i : Ξ±) β†’ Ξ² i
piecewise
(
c: Ξ±
c
β€’
f₁: (i : I) β†’ f i
f₁
) (
c: Ξ±
c
β€’
g₁: (i : I) β†’ f i
g₁
) =
c: Ξ±
c
β€’
s: Set I
s
.
piecewise: {Ξ± : Type ?u.34734} β†’ {Ξ² : Ξ± β†’ Sort ?u.34733} β†’ (s : Set Ξ±) β†’ ((i : Ξ±) β†’ Ξ² i) β†’ ((i : Ξ±) β†’ Ξ² i) β†’ [inst : (j : Ξ±) β†’ Decidable (j ∈ s)] β†’ (i : Ξ±) β†’ Ξ² i
piecewise
f₁: (i : I) β†’ f i
f₁
g₁: (i : I) β†’ f i
g₁
:=
s: Set I
s
.
piecewise_op: βˆ€ {Ξ± : Type ?u.34820} {Ξ΄ : Ξ± β†’ Sort ?u.34821} (s : Set Ξ±) (f g : (i : Ξ±) β†’ Ξ΄ i) [inst : (j : Ξ±) β†’ Decidable (j ∈ s)] {Ξ΄' : Ξ± β†’ Sort ?u.34819} (h : (i : Ξ±) β†’ Ξ΄ i β†’ Ξ΄' i), (piecewise s (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (piecewise s f g x)
piecewise_op
(Ξ΄' :=
f: I β†’ Type v
f
)
f₁: (i : I) β†’ f i
f₁
_: (i : ?m.34830) β†’ ?m.34831 i
_
fun
_: ?m.34857
_
=>
(Β· β€’ Β·): Ξ± β†’ f x✝ β†’ f x✝
(Β· β€’ Β·)
c: Ξ±
c
#align set.piecewise_smul
Set.piecewise_smul: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ SMul Ξ± (f i)] (s : Set I) [inst_1 : (i : I) β†’ Decidable (i ∈ s)] (c : Ξ±) (f₁ g₁ : (i : I) β†’ f i), piecewise s (c β€’ f₁) (c β€’ g₁) = c β€’ piecewise s f₁ g₁
Set.piecewise_smul
#align set.piecewise_vadd
Set.piecewise_vadd: βˆ€ {I : Type u} {f : I β†’ Type v} {Ξ± : Type u_1} [inst : (i : I) β†’ VAdd Ξ± (f i)] (s : Set I) [inst_1 : (i : I) β†’ Decidable (i ∈ s)] (c : Ξ±) (f₁ g₁ : (i : I) β†’ f i), piecewise s (c +α΅₯ f₁) (c +α΅₯ g₁) = c +α΅₯ piecewise s f₁ g₁
Set.piecewise_vadd
end Set section Extend @[
to_additive: βˆ€ {R : Type u_1} {Ξ± : Type u_2} {Ξ² : Type u_3} {Ξ³ : Type u_4} [inst : VAdd R Ξ³] (r : R) (f : Ξ± β†’ Ξ²) (g : Ξ± β†’ Ξ³) (e : Ξ² β†’ Ξ³), extend f (r +α΅₯ g) (r +α΅₯ e) = r +α΅₯ extend f g e
to_additive
] theorem
Function.extend_smul: βˆ€ {R : Type u_1} {Ξ± : Type u_2} {Ξ² : Type u_3} {Ξ³ : Type u_4} [inst : SMul R Ξ³] (r : R) (f : Ξ± β†’ Ξ²) (g : Ξ± β†’ Ξ³) (e : Ξ² β†’ Ξ³), extend f (r β€’ g) (r β€’ e) = r β€’ extend f g e
Function.extend_smul
{
R: Type u_1
R
Ξ±: Type ?u.35279
Ξ±
Ξ²: Type ?u.35282
Ξ²
Ξ³: Type ?u.35285
Ξ³
:
Type _: Type (?u.35279+1)
Type _
} [
SMul: Type ?u.35289 β†’ Type ?u.35288 β†’ Type (max?u.35289?u.35288)
SMul
R: Type ?u.35276
R
Ξ³: Type ?u.35285
Ξ³
] (
r: R
r
:
R: Type ?u.35276
R
) (
f: Ξ± β†’ Ξ²
f
:
Ξ±: Type ?u.35279
Ξ±
β†’
Ξ²: Type ?u.35282
Ξ²
) (
g: Ξ± β†’ Ξ³
g
:
Ξ±: Type ?u.35279
Ξ±
β†’
Ξ³: Type ?u.35285
Ξ³
) (
e: Ξ² β†’ Ξ³
e
:
Ξ²: Type ?u.35282
Ξ²
β†’
Ξ³: Type ?u.35285
Ξ³
) :
Function.extend: {Ξ± : Sort ?u.35309} β†’ {Ξ² : Sort ?u.35308} β†’ {Ξ³ : Sort ?u.35307} β†’ (Ξ± β†’ Ξ²) β†’ (Ξ± β†’ Ξ³) β†’ (Ξ² β†’ Ξ³) β†’ Ξ² β†’ Ξ³
Function.extend
f: Ξ± β†’ Ξ²
f
(
r: R
r
β€’
g: Ξ± β†’ Ξ³
g
) (
r: R
r
β€’
e: Ξ² β†’ Ξ³
e
) =
r: R
r
β€’
Function.extend: {Ξ± : Sort ?u.35479} β†’ {Ξ² : Sort ?u.35478} β†’ {Ξ³ : Sort ?u.35477} β†’ (Ξ± β†’ Ξ²) β†’ (Ξ± β†’ Ξ³) β†’ (Ξ² β†’ Ξ³) β†’ Ξ² β†’ Ξ³
Function.extend
f: Ξ± β†’ Ξ²
f
g: Ξ± β†’ Ξ³
g
e: Ξ² β†’ Ξ³
e
:=
funext: βˆ€ {Ξ± : Sort ?u.35565} {Ξ² : Ξ± β†’ Sort ?u.35564} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext
fun
x: ?m.35579
x
=>

Goals accomplished! πŸ™
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²


extend f (r β€’ g) (r β€’ e) x = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


extend f (r β€’ g) (r β€’ e) x = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²


extend f (r β€’ g) (r β€’ e) x = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


extend f (r β€’ g) (r β€’ e) x = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


(if h : βˆƒ a, f a = x then (r β€’ g) (Classical.choose h) else (r β€’ e) x) = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


extend f (r β€’ g) (r β€’ e) x = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


(if h : βˆƒ a, f a = x then (r β€’ g) (Classical.choose h) else r β€’ e x) = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


extend f (r β€’ g) (r β€’ e) x = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


(if h : βˆƒ a, f a = x then (r β€’ g) (Classical.choose h) else r β€’ e x) = r β€’ extend f g e x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


extend f (r β€’ g) (r β€’ e) x = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


(if h : βˆƒ a, f a = x then (r β€’ g) (Classical.choose h) else r β€’ e x) = r β€’ if h : βˆƒ a, f a = x then g (Classical.choose h) else e x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


(if h : βˆƒ a, f a = x then (r β€’ g) (Classical.choose h) else r β€’ e x) = r β€’ if h : βˆƒ a, f a = x then g (Classical.choose h) else e x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²


extend f (r β€’ g) (r β€’ e) x = (r β€’ extend f g e) x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)

h✝: βˆƒ a, f a = x


inl
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)

h✝: Β¬βˆƒ a, f a = x


inr
r β€’ e x = r β€’ e x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


(if h : βˆƒ a, f a = x then (r β€’ g) (Classical.choose h) else r β€’ e x) = r β€’ if h : βˆƒ a, f a = x then g (Classical.choose h) else e x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)

h✝: βˆƒ a, f a = x


inl
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)

h✝: Β¬βˆƒ a, f a = x


inr
r β€’ e x = r β€’ e x
I: Type u

f✝: I β†’ Type v

x✝, y: (i : I) β†’ f✝ i

i: I

R: Type u_1

Ξ±: Type u_2

Ξ²: Type u_3

Ξ³: Type u_4

inst✝: SMul R γ

r: R

f: Ξ± β†’ Ξ²

g: Ξ± β†’ Ξ³

e: Ξ² β†’ Ξ³

x: Ξ²

this: Decidable (βˆƒ a, f a = x)


(if h : βˆƒ a, f a = x then (r β€’ g) (Classical.choose h) else r β€’ e x) = r β€’ if h : βˆƒ a, f a = x then g (Classical.choose h) else e x

Goals accomplished! πŸ™
-- convert (apply_dite (fun c : Ξ³ => r β€’ c) _ _ _).symm #align function.extend_smul
Function.extend_smul: βˆ€ {R : Type u_1} {Ξ± : Type u_2} {Ξ² : Type u_3} {Ξ³ : Type u_4} [inst : SMul R Ξ³] (r : R) (f : Ξ± β†’ Ξ²) (g : Ξ± β†’ Ξ³) (e : Ξ² β†’ Ξ³), Function.extend f (r β€’ g) (r β€’ e) = r β€’ Function.extend f g e
Function.extend_smul
#align function.extend_vadd
Function.extend_vadd: βˆ€ {R : Type u_1} {Ξ± : Type u_2} {Ξ² : Type u_3} {Ξ³ : Type u_4} [inst : VAdd R Ξ³] (r : R) (f : Ξ± β†’ Ξ²) (g : Ξ± β†’ Ξ³) (e : Ξ² β†’ Ξ³), Function.extend f (r +α΅₯ g) (r +α΅₯ e) = r +α΅₯ Function.extend f g e
Function.extend_vadd
end Extend