Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-06 12:41 8cebd2b1

View on Github →

chore(algebra/algebra): Split subalgebras into their own file (#4471) This matches how subring and submonoid both have their own files. This also remove noncomputable theory which is unnecessary for almost all the definitions

Estimated changes

deleted theorem alg_hom.coe_range
deleted theorem alg_hom.mem_range
deleted def algebra.adjoin
deleted def algebra.bot_equiv
deleted theorem algebra.coe_bot
deleted theorem algebra.coe_top
deleted theorem algebra.comap_top
deleted theorem algebra.eq_top_iff
deleted theorem algebra.map_bot
deleted theorem algebra.map_top
deleted theorem algebra.mem_bot
deleted theorem algebra.mem_top
deleted def algebra.to_top
deleted theorem mem_subalgebra_of_subring
deleted theorem subalgebra.add_mem
deleted theorem subalgebra.coe_int_mem
deleted theorem subalgebra.coe_nat_mem
deleted theorem subalgebra.coe_val
deleted def subalgebra.comap'
deleted def subalgebra.comap
deleted theorem subalgebra.ext
deleted theorem subalgebra.ext_iff
deleted theorem subalgebra.gsmul_mem
deleted theorem subalgebra.list_prod_mem
deleted theorem subalgebra.list_sum_mem
deleted def subalgebra.map
deleted theorem subalgebra.map_injective
deleted theorem subalgebra.map_le
deleted theorem subalgebra.map_mono
deleted theorem subalgebra.mem_coe
deleted theorem subalgebra.mem_map
deleted theorem subalgebra.mul_mem
deleted theorem subalgebra.neg_mem
deleted theorem subalgebra.nsmul_mem
deleted theorem subalgebra.one_mem
deleted theorem subalgebra.pow_mem
deleted theorem subalgebra.prod_mem
deleted theorem subalgebra.range_le
deleted theorem subalgebra.range_subset
deleted theorem subalgebra.range_val
deleted theorem subalgebra.smul_mem
deleted theorem subalgebra.srange_le
deleted theorem subalgebra.sub_mem
deleted theorem subalgebra.sum_mem
deleted def subalgebra.under
deleted def subalgebra.val
deleted theorem subalgebra.val_apply
deleted theorem subalgebra.zero_mem
deleted structure subalgebra
added theorem alg_hom.coe_range
added theorem alg_hom.mem_range
added def algebra.adjoin
added theorem algebra.coe_bot
added theorem algebra.coe_top
added theorem algebra.comap_top
added theorem algebra.eq_top_iff
added theorem algebra.map_bot
added theorem algebra.map_top
added theorem algebra.mem_bot
added theorem algebra.mem_top
added def algebra.to_top
added theorem subalgebra.add_mem
added theorem subalgebra.coe_int_mem
added theorem subalgebra.coe_nat_mem
added theorem subalgebra.coe_val
added def subalgebra.comap
added theorem subalgebra.ext
added theorem subalgebra.ext_iff
added theorem subalgebra.gsmul_mem
added def subalgebra.map
added theorem subalgebra.map_le
added theorem subalgebra.map_mono
added theorem subalgebra.mem_coe
added theorem subalgebra.mem_map
added 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
added theorem subalgebra.range_le
added theorem subalgebra.range_val
added theorem subalgebra.smul_mem
added theorem subalgebra.srange_le
added theorem subalgebra.sub_mem
added theorem subalgebra.sum_mem
added def subalgebra.under
added def subalgebra.val
added theorem subalgebra.val_apply
added theorem subalgebra.zero_mem
added structure subalgebra