Mathlib v3 is deprecated. Go to Mathlib v4

Def test.wlr_irred

Modification history

2020-05-29 16:24

test/with_local_reducibility.lean

feat(tactic/with_local_reducibility): alter reducibility attributes locally (#2820)

Added test.wlr_irred View on Github →