`BookProof.conjugateli_trans` (Θ : E ≃ₗᵢ[R] E') (A B : E ≃ₗᵢ[R] E) : conjugateₗᵢ Θ (A.trans B) = (conjugateₗᵢ Θ A).trans (conjugateₗᵢ Θ B)

Initializing...

`BookProof.conjugateli_trans` (Θ : E ≃ₗᵢ[R] E') (A B : E ≃ₗᵢ[R] E) : conjugateₗᵢ Θ (A.trans B) = (conjugateₗᵢ Θ A).trans (conjugateₗᵢ Θ B) · Prove2Me