defs): Declare `field_simps` attribute earlier (#13543)

Commit

4 years ago

chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543) Declaring `field_simps` earlier make the relevant lemmas taggable as they are declared.

Author

YaelDillies

Parents

b2518bee

mathlib c93b99fa - chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543)

mathlib
c93b99fa - chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543)