case a.h
ι : Type u_1
ι' : Type ?u.170437
κ : Type ?u.170440
κ' : Type ?u.170443
R : Type ?u.170446
M : Type ?u.170449
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_2
M₂ : Type u_3
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j
ι : Type u_1
ι' : Type ?u.170437
κ : Type ?u.170440
κ' : Type ?u.170443
R : Type ?u.170446
M : Type ?u.170449
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_2
M₂ : Type u_3
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
⊢ toMatrix e ↑(unitsSMul e w) = Matrix.diagonal (Units.val ∘ w)
ext (i j)
case pos
ι : Type u_1
ι' : Type ?u.170437
κ : Type ?u.170440
κ' : Type ?u.170443
R : Type ?u.170446
M : Type ?u.170449
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_2
M₂ : Type u_3
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : i = j
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j

case neg
ι : Type u_1
ι' : Type ?u.170437
κ : Type ?u.170440
κ' : Type ?u.170443
R : Type ?u.170446
M : Type ?u.170449
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_2
M₂ : Type u_3
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : ¬i = j
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j
case a.h
ι : Type u_1
ι' : Type ?u.170437
κ : Type ?u.170440
κ' : Type ?u.170443
R : Type ?u.170446
M : Type ?u.170449
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_2
M₂ : Type u_3
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j
by_cases h : i = j
no goals
case pos
ι : Type u_1
ι' : Type ?u.170437
κ : Type ?u.170440
κ' : Type ?u.170443
R : Type ?u.170446
M : Type ?u.170449
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_2
M₂ : Type u_3
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : i = j
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j
simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]
no goals
case neg
ι : Type u_1
ι' : Type ?u.170437
κ : Type ?u.170440
κ' : Type ?u.170443
R : Type ?u.170446
M : Type ?u.170449
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_2
M₂ : Type u_3
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : ¬i = j
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j
simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def, Ne.symm h]