Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-08 14:31 f90fcc9e

View on Github →

chore(*): use is_algebra_tower instead of algebra.comap and generalize some constructions to semirings (#3299) algebra.comap is now reserved to the creation of new algebra instances. For assumptions of theorems / constructions, is_algebra_tower is the new way to do it. For example:

variables [algebra K L] [algebra L A]
lemma is_algebraic_trans (L_alg : is_algebraic K L) (A_alg : is_algebraic L A) :
  is_algebraic K (comap K L A) :=

is now written as:

variables [algebra K L] [algebra L A] [algebra K A] [is_algebra_tower K L A]
lemma is_algebraic_trans (L_alg : is_algebraic K L) (A_alg : is_algebraic L A) :
  is_algebraic K A :=

Estimated changes

modified theorem linear_map.map_neg₂
modified def tensor_product.map
modified def tensor_product.mk
modified theorem algebra.adjoin_int
added theorem algebra.mem_adjoin_iff
added def alg_hom_nat
added theorem span_nat_eq
added theorem subalgebra.add_mem
added theorem subalgebra.coe_int_mem
added theorem subalgebra.coe_nat_mem
added theorem subalgebra.gsmul_mem
modified theorem subalgebra.mul_mem
added theorem subalgebra.neg_mem
added theorem subalgebra.nsmul_mem
added theorem subalgebra.one_mem
added theorem subalgebra.pow_mem
added theorem subalgebra.prod_mem
modified theorem subalgebra.range_le
added theorem subalgebra.smul_mem
added theorem subalgebra.srange_le
added theorem subalgebra.sub_mem
added theorem subalgebra.sum_mem
modified def subalgebra.under
added theorem subalgebra.zero_mem
modified theorem submodule.map_mul
added theorem is_integral_alg_hom
modified theorem is_integral_trans_aux
modified theorem subsemiring.ext