Documentation
Monlib
.
Preq
.
Dite
Search
return to top
source
Imports
Init
Mathlib.Logic.Basic
Mathlib.Algebra.Group.Defs
Mathlib.Algebra.Star.Basic
Mathlib.LinearAlgebra.TensorProduct.Basic
Imported by
hMul_dite
dite_hMul
dite_boole_add
dite_boole_smul
star_dite
dite_tmul
tmul_dite
LinearMap
.
apply_dite
dite_apply'
Some stuff on dites
#
source
theorem
hMul_dite
{
α
:
Type
u_1}
[
Mul
α
]
(
P
:
Prop
)
[
Decidable
P
]
(
a
:
α
)
(
b
:
P
→
α
)
(
c
:
¬
P
→
α
)
:
(
a
*
if x :
P
then
b
x
else
c
x
)
=
if x :
P
then
a
*
b
x
else
a
*
c
x
source
theorem
dite_hMul
{
α
:
Type
u_1}
[
Mul
α
]
(
P
:
Prop
)
[
Decidable
P
]
(
a
:
α
)
(
b
:
P
→
α
)
(
c
:
¬
P
→
α
)
:
(if x :
P
then
b
x
else
c
x
)
*
a
=
if x :
P
then
b
x
*
a
else
c
x
*
a
source
theorem
dite_boole_add
{
α
:
Type
u_1}
[
AddZeroClass
α
]
(
P
:
Prop
)
[
Decidable
P
]
(
a
b
:
P
→
α
)
:
(if x :
P
then
a
x
+
b
x
else
0
)
=
(if x :
P
then
a
x
else
0
)
+
if x :
P
then
b
x
else
0
source
theorem
dite_boole_smul
{
α
:
Type
u_1}
{
β
:
Type
u_2}
[
Zero
α
]
[
SMulZeroClass
β
α
]
(
P
:
Prop
)
[
Decidable
P
]
(
a
:
P
→
α
)
(
r
:
β
)
:
(if x :
P
then
r
•
a
x
else
0
)
=
r
•
if x :
P
then
a
x
else
0
source
theorem
star_dite
(
P
:
Prop
)
[
Decidable
P
]
{
α
:
Type
u_1}
[
InvolutiveStar
α
]
(
a
:
P
→
α
)
(
b
:
¬
P
→
α
)
:
star
(if i :
P
then
a
i
else
b
i
)
=
if i :
P
then
star
(
a
i
)
else
star
(
b
i
)
source
theorem
dite_tmul
{
R
:
Type
u_1}
{
N₁
:
Type
u_2}
{
N₂
:
Type
u_3}
[
CommSemiring
R
]
[
AddCommGroup
N₁
]
[
AddCommGroup
N₂
]
[
Module
R
N₁
]
[
Module
R
N₂
]
(
P
:
Prop
)
[
Decidable
P
]
(
x₁
:
P
→
N₁
)
(
x₂
:
N₂
)
:
(if h :
P
then
x₁
h
else
0
)
⊗ₜ[
R
]
x₂
=
if h :
P
then
x₁
h
⊗ₜ[
R
]
x₂
else
0
source
theorem
tmul_dite
{
R
:
Type
u_1}
{
N₁
:
Type
u_2}
{
N₂
:
Type
u_3}
[
CommSemiring
R
]
[
AddCommGroup
N₁
]
[
AddCommGroup
N₂
]
[
Module
R
N₁
]
[
Module
R
N₂
]
(
P
:
Prop
)
[
Decidable
P
]
(
x₁
:
N₁
)
(
x₂
:
P
→
N₂
)
:
(
x₁
⊗ₜ[
R
]
if h :
P
then
x₂
h
else
0
)
=
if h :
P
then
x₁
⊗ₜ[
R
]
x₂
h
else
0
source
theorem
LinearMap
.
apply_dite
{
R
:
Type
u_1}
{
H₁
:
Type
u_2}
{
H₂
:
Type
u_3}
[
Semiring
R
]
[
AddCommMonoid
H₁
]
[
AddCommMonoid
H₂
]
[
Module
R
H₁
]
[
Module
R
H₂
]
(
f
:
H₁
→ₗ[
R
]
H₂
)
(
P
:
Prop
)
[
Decidable
P
]
(
a
:
P
→
H₁
)
(
b
:
¬
P
→
H₁
)
:
f
(if h :
P
then
a
h
else
b
h
)
=
if h :
P
then
f
(
a
h
)
else
f
(
b
h
)
source
theorem
dite_apply'
{
i
:
Type
u_1}
{
β
:
Type
u_2}
{
α
:
i
→
Type
u_3
}
(
P
:
Prop
)
[
Decidable
P
]
{
j
:
i
}
(
f
:
P
→
β
→
α
j
)
[
Zero
(
α
j
)
]
(
a
:
β
)
:
(if h :
P
then
f
h
else
0
)
a
=
if h :
P
then
f
h
a
else
0