Adjoining elements to form subalgebras #
This file develops the basic theory of subalgebras of an R-algebra generated
by a set of elements. A basic interface for adjoin
is set up.
Tags #
adjoin, algebra
Induction principle for the algebra generated by a set s
: show that p x y
holds for any
x y ∈ adjoin R s
given that it holds for x y ∈ s
and that it satisfies a number of
natural properties.
The difference with Algebra.adjoin_induction
is that this acts on the subtype.
If all elements of s : Set A
commute pairwise, then adjoin R s
is a commutative
semiring.
Instances For
If all elements of s : Set A
commute pairwise, then adjoin R s
is a commutative
ring.
Instances For
The ℕ
-algebra equivalence between Subsemiring.closure s
and Algebra.adjoin ℕ s
given
by the identity map.
Instances For
The ℤ
-algebra equivalence between Subring.closure s
and Algebra.adjoin ℤ s
given by
the identity map.