mathlib

042c290d - refactor(category_theory/opposites): Make `opposite` irreducible