Commit 2024-10-23 11:27 dcd264a6

View on Github →

feat(Algebra/Irreducible): prove irreducibility preserved by MulEquiv (#17092) Add two lemmas about Irreducibility preserved by MulEquiv.

Estimated changes

added theorem Irreducible.map