Theorem map_dvd_iff_dvd_symm

Modification history

2025-05-22 12:54

Mathlib/Algebra/Ring/Divisibility/Basic.lean

feat(UniqueFactorizationMonoid): a `MulEquiv` that commutes with `normalize` preserves `normalizedFactors` (#25080)

Added map_dvd_iff_dvd_symm View on Github →