Classifies porting notes claiming:
removed @[pp_nodot]
Examples
|
/-- The element of `SymAlg α` that represents `a : α`. -/ |
|
@[match_pattern] |
|
-- Porting note: removed @[pp_nodot] |
|
def sym : α ≃ αˢʸᵐ := |
|
Equiv.refl _ |
|
#align sym_alg.sym SymAlg.sym |
|
|
|
/-- The element of `α` represented by `x : αˢʸᵐ`. -/ |
|
-- Porting note: removed @[pp_nodot] |
|
def unsym : αˢʸᵐ ≃ α := |
Classifies porting notes claiming:
Examples
mathlib4/Mathlib/Algebra/Symmetrized.lean
Lines 48 to 57 in 2a65c8d