Commit 2021-04-21 00:48 ad588611

refactor(group_theory/submonoid): adjust definitional unfolding of add_monoid_hom.mrange to match set.range (#7227) This changes the following to unfold to set.range:

• monoid_hom.mrange
• add_monoid_hom.mrange
• linear_map.range
• lie_hom.range
• ring_hom.range
• ring_hom.srange
• ring_hom.field_range
• alg_hom.range For example:

import ring_theory.subring
variables (R : Type*) [ring R] (f : R →+* R)
-- before this PR, these required `f '' univ` on the RHS
example : (f.range : set R) = set.range f := rfl
example : (f.srange : set R) = set.range f := rfl
example : (f.to_monoid_hom.mrange : set R) = set.range f := rfl
-- this one is unchanged by this PR
example : (f.to_add_monoid_hom.range : set R) = set.range f := rfl

The motivations behind this change are that

• It eliminates a lot of ∈ set.univ hypotheses and goals that are just annoying
• it means that an equivalence like A ≃ set.range f is defeq to A ≃ f.range, with no need to insert awkward equiv.cast-like terms to translate between different approaches
• monoid_hom.range (as opposed to mrange) already used this pattern. The number of lines has gone up a bit, but most of those are comments explaining the design choice. Zulip