Theorem GradedMonoid.fst_one

Modification history

2023-12-23 00:28

Mathlib/Algebra/GradedMonoid.lean

feat(Algebra/GradedMonoid): missing lemmas about `fst` and `snd` (#9227)

Added GradedMonoid.fst_one View on Github →