Commits leanprover-community/mathlib

Prove very convenient lemmas

vihdzp committed 4 years ago

30ce4bcd

Let's try again

vihdzp committed 4 years ago

90ead26e

feat(set_theory/ordinal_arithmetic): Suprema of empty families (#11872)

vihdzp committed 4 years ago

e18972b3

feat(group_theory/sylow): the cardinality of a sylow group (#11776)

nomeata committed 4 years ago

24ebc5cd

feat(set_theory/ordinal_arithmetic): Suprema and least strict upper bounds of constant families (#11862)

vihdzp committed 4 years ago

4148990d

feat(category_theory): a hierarchy of balanced categories (#11856)

TwoFX committed 4 years ago

6787a8d9

feat(algebra/cubic_discriminant): basics of cubic polynomials and their discriminants (#11483)

Multramate committed 4 years ago

0f9c1538

feat(algebra/lie/nilpotent): nilpotency of Lie modules depends only on the Lie subalgebra of linear endomorphisms (#11853)

ocfnash committed 4 years ago

39b12623

feat(algebra/lie/nilpotent): nilpotency of Lie modules is preserved under surjective morphisms (#11852)

ocfnash committed 4 years ago

b9d19ed3

feat(algebra/lie/nilpotent): add lemma `lie_module.coe_lower_central_series_ideal_le` (#11851)

ocfnash committed 4 years ago

9fcd1f24

feat(algebra/lie/nilpotent): add definition `lie_ideal.lcs` (#11854)

ocfnash committed 4 years ago

df7c217f

feat(measure_theory/probability_mass_function): Lemmas connecting `pmf.support` and `pmf.to_measure` (#11842)

dtumad committed 4 years ago

99693218

feat(data/finset): erase is empty iff (#11838)

b-mehta committed 4 years ago

612ca40a

refactor(ring_theory/valuation/basic): `fun_like` design for `valuation` (#11830)

YaelDillies committed 4 years ago

31f5688a

feat(ring_theory/power_series): reindex trunc of a power series to truncate below index n (#10891)

alexjbest committed 4 years ago

e78563c0

chore(data/fintype/basic): rename some instances (#11845)

urkud committed 4 years ago

6b4e2691

feat(ring_theory/hahn_series): add a map to power series and dickson's lemma (#11836)

alexjbest committed 4 years ago

b0d9761b

feat(ring_theory/nilpotent): add lemma `module.End.is_nilpotent_mapq` (#11831)

ocfnash committed 4 years ago

bd7d034b

fix(group_theory/nilpotent): don’t unnecessarily `open_locale classical` (#11779)

nomeata committed 4 years ago

b905eb66

feat(algebra/lie/quotient): first isomorphism theorem for morphisms of Lie algebras (#11826)

ocfnash committed 4 years ago

b3b32c87

feat(algebra/lie/ideal_operations): add lemma `lie_ideal_oper_eq_linear_span'` (#11823)

ocfnash committed 4 years ago

292bf34d

feat(linear_algebra/basic): add minor lemmas, tweak `simp` attributes (#11822)

ocfnash committed 4 years ago

fa204820

feat(algebra/lie/cartan_subalgebra): add lemma `lie_subalgebra.exists_nested_lie_ideal_of_le_normalizer` (#11820)

ocfnash committed 4 years ago

247504c8

feat(algebra/lie/basic): define pull back of a Lie module along a morphism of Lie algebras. (#11819)

ocfnash committed 4 years ago

a2fd0bd5

refactor(set_theory/ordinal_arithmetic): Change `α → Prop` to `set α` (#11816)

vihdzp committed 4 years ago

2e7efe99

chore(algebra/group): make `coe_norm_subgroup` and `submodule.norm_coe` consistent (#11427)

Vierkantor committed 4 years ago

a7415855

feat(algebra/lie/subalgebra): add `lie_subalgebra.equiv_of_le` and `lie_subalgebra.equiv_range_of_injective` (#11828)

ocfnash committed 4 years ago

c3273aa2

fix(algebra/Module/colimits): Change `comm_ring` to `ring`. (#11837)

adamtopaz committed 4 years ago

3c00e5d7

refactor(analysis/normed_space/add_torsor): Kill `seminormed_add_torsor` (#11795)

YaelDillies committed 4 years ago

5b3cd4a9

feat(category_theory/category/{Pointed,Bipointed}): The categories of pointed/bipointed types (#11777)

YaelDillies committed 4 years ago

aaaeeaed