Theorem Pi.inv_apply

Modification history

2026-10-29 15:19
Mathlib/Algebra/Notation/Pi/Defs.lean
chore: protect `Pi.*_apply` lemmas (#45435) …
Deleted Pi.inv_applyView on Github →
2025-05-25 18:26
Mathlib/Algebra/Notation/Pi.lean
chore(Algebra/Notation/Pi): improve variable names (#25040) …
Modified Pi.inv_applyView 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 Pi.inv_applyView on Github →
2022-11-28 15:54
Mathlib/Data/Pi/Algebra.lean
feat: port Data.Pi.Algebra (#564) …
Added Pi.inv_applyView on Github →