case C0
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun R A n (↑(toFunAlgHom R A n) 0) = 0

case C1
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
m : Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) (a ⊗ₜ[R] m)) = a ⊗ₜ[R] m

case Cp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) (x + y)) = x + y
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : A ⊗[R] Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) M) = M
induction' M using TensorProduct.induction_on with a m x y hx hy
no goals
case C0
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun R A n (↑(toFunAlgHom R A n) 0) = 0
simp
no goals
case C1
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
m : Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) (a ⊗ₜ[R] m)) = a ⊗ₜ[R] m
simp
case Cp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) x + ↑(toFunAlgHom R A n) y) = x + y
case Cp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) (x + y)) = x + y
rw [map_add]
no goals
case Cp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) x + ↑(toFunAlgHom R A n) y) = x + y
conv_rhs => rw [← hx, ← hy, ← invFun_add]