Theorem Function.const_one

Modification history

2025-05-25 18:26
Mathlib/Algebra/Notation/Pi.lean
chore(Algebra/Notation/Pi): improve variable names (#25040) …
Modified Function.const_oneView on Github →
2025-03-03 23:07
Mathlib/Algebra/Group/Pi/Basic.lean
chore(Algebra/Group/Pi): separate notation from the other instances (#22499) …
Modified Function.const_oneView on Github →
2024-02-13 19:40
Mathlib/Data/Pi/Algebra.lean
chore: Move lemmas about `Function.const` to the `Function` namespace (#10220) …
Added Function.const_oneView on Github →