[Merged by Bors] - chore(linear_algebra/basic): generalize add_monoid_hom_lequiv_{nat,int}

[eric-wieser]

---

cc @riccardobrasca

[riccardobrasca]

LGTM

[riccardobrasca]

Maybe it is reasonable to add some compatibility when we have R S M [algebra R S] [module R M] [module S M] [is_scalar_tower R S M] ...

[eric-wieser]

I'm not sure I understand what you mean by your second comment - the choice of R is entirely free, there is no need to add any extra variables.

[riccardobrasca]

I mean the following

example {A B : Type*} (R : Type*) (S : Type*) [comm_semiring R] [semiring S] [algebra R S]
  [add_comm_group A] [add_comm_group B] [module R B] [module S B] [is_scalar_tower R S B] :
  linear_equiv.restrict_scalars R (add_monoid_hom_lequiv_int S) =
  (add_monoid_hom_lequiv_int R : (A →+ B) ≃ₗ[R] (A →ₗ[ℤ] B)) := rfl

[eric-wieser]

While harmless, I don't think that's really worth it; there are probably 10s of defs missing .restrict_scalars lemmas like that.

Having said that, if you find yourself needing that type of lemma I'm happy to approve a PR adding them (but note your assumptions are too strong there, linear_equiv.restrict_scalars does not require an algebra)

[urkud]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests