Commit 2026-09-29 15:37 5e043698

feat(RepresentationTheory): add two simp lemmas (#43649) We add two simp lemmas saying both the composition and precomposition with zero are zero

@[simp]
lemma comp_zero (f : IntertwiningMap σ τ) :
    comp f (0 : IntertwiningMap ρ σ) = 0 := by ext; simp
@[simp]
lemma zero_comp (g : IntertwiningMap ρ σ) :
    comp (0 : IntertwiningMap σ τ) g = 0 := by ext; simp

We also fix the names add_comp and comp_add