@[reduce_mod_char]
attribute #
This file registers @[reduce_mod_char]
as a simp
attribute.
@[reduce_mod_char]
is an attribute that tags lemmas for preprocessing and cleanup in the
reduce_mod_char
tactic
Mathlib.Tactic.ReduceModChar.Ext
@[reduce_mod_char]
attribute #This file registers @[reduce_mod_char]
as a simp
attribute.
@[reduce_mod_char]
is an attribute that tags lemmas for preprocessing and cleanup in the
reduce_mod_char
tactic