Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-05 11:57 23270e71

View on Github →

feat(ring_theory/adjoin): adjoining elements to form subalgebras (#756)

  • feat(ring_theory/adjoin): adjoining elements to form subalgebras
  • Fix build
  • Change to_submodule into a coercion
  • Use pointwise_mul
  • add simp attribute to adjoin_empty

Estimated changes

added theorem algebra.adjoin_empty
added theorem algebra.adjoin_eq_span
added theorem algebra.adjoin_int
added theorem algebra.adjoin_le
added theorem algebra.adjoin_le_iff
added theorem algebra.adjoin_mono
added theorem algebra.adjoin_union
added theorem algebra.fg_trans
added theorem algebra.subset_adjoin
added def subalgebra.fg
added theorem subalgebra.fg_bot
added theorem subalgebra.fg_def