no goals
l : Type ?u.83546
m : Type ?u.83549
n : Type u_1
o : Type ?u.83555
m' : o → Type ?u.83560
n' : o → Type ?u.83565
R : Type ?u.83568
S : Type ?u.83571
α : Type v
β : Type w
γ : Type ?u.83578
inst✝² : DecidableEq n
inst✝¹ : AddZeroClass α
inst✝ : One α
M : Matrix n n α
i j : n
h : i ≠ j
⊢ bit1 M i j = bit0 (M i j)
simp [bit1_apply, h]