`BookProof.ChapterIPin.ipin_right` (Λ : P →* Multiplicative (AddAut V)) (x y : IPin Λ) : (x * y).right = x.right * y.right

Initializing...

`BookProof.ChapterIPin.ipin_right` (Λ : P →* Multiplicative (AddAut V)) (x y : IPin Λ) : (x * y).right = x.right * y.right · Prove2Me