Theorem: Matrix.hom_conj (Logic/Logic/LogicSymbol.lean)

State before:
β : Type u_3
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
n : ℕ
inst✝¹ : FunLike F α β
inst✝ : LogicalConnective.HomClass F α β
f : F
v : Fin n → α
⊢ f (conj v) = conj (⇑f ∘ v)
Tactic:
induction' n with n ih <;> simp[*, conj]
State after:
no goals