Zulip Chat Archive

Stream: Is there code for X?

Topic: constructing `subalgebra` without duplicate axioms


view this post on Zulip Eric Wieser (Feb 25 2021 at 19:35):

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?

view this post on Zulip Eric Wieser (Feb 25 2021 at 19:40):

Seems to work: #6417


Last updated: May 07 2021 at 21:10 UTC