Theorem symmetric_isRelPrime

Modification history

2026-06-10 08:59

Mathlib/Algebra/Divisibility/Units.lean

chore(Order/Defs/Unbundled): deprecate `def Symmetric` in favor of `class Std.Symm` (#38092)

Deleted symmetric_isRelPrime View on Github →

2025-06-01 19:52

Mathlib/Algebra/Divisibility/Units.lean

feat(RingTheory/Radical): generalise and fill in TODOs (#25335) …

Added symmetric_isRelPrime View on Github →