mathlib
1bf41817 - feat(data/equiv/{basic,mul_equiv)}: add Pi_subsingleton (#12040)

Commit

3 years ago

feat(data/equiv/{basic,mul_equiv)}: add Pi_subsingleton (#12040)

Author

nomeata

nomeata

Parents

Loading