constructing `subalgebra` without duplicate axioms

Stream: Is there code for X?

[Eric Wieser]

Does this exist?

import algebra.algebra.subalgebra

variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]

example
  (s : set A)
  (algebra_map_mem : ∀ r, algebra_map R A r ∈ s)
  (mul_mem : ∀ a b, a ∈ s → b ∈ s → (a * b) ∈ s)
  (add_mem : ∀ a b, a ∈ s → b ∈ s → (a + b) ∈ s) :
  subalgebra R A :=
{ carrier := s,
  zero_mem' := (algebra_map R A).map_zero ▸ algebra_map_mem 0,
  one_mem' := (algebra_map R A).map_one ▸ algebra_map_mem 1,
  add_mem' := add_mem,
  mul_mem' := mul_mem,
  algebra_map_mem' := algebra_map_mem }

Would it make sense to make fields of subalgebra autoparams?

[Eric Wieser]

Seems to work: #6417