Commits leanprover-community/mathlib

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

Multramate committed 3 years ago

0f9c1538

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

ocfnash committed 3 years ago

39b12623

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

ocfnash committed 3 years ago

b9d19ed3

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

ocfnash committed 3 years ago

9fcd1f24

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

ocfnash committed 3 years ago

df7c217f

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

dtumad committed 3 years ago

99693218

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

b-mehta committed 3 years ago

612ca40a

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

YaelDillies committed 3 years ago

31f5688a

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

alexjbest committed 3 years ago

e78563c0

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

urkud committed 3 years ago

6b4e2691

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

alexjbest committed 3 years ago

b0d9761b

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

ocfnash committed 3 years ago

bd7d034b

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

nomeata committed 3 years ago

b905eb66

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

ocfnash committed 3 years ago

b3b32c87

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

ocfnash committed 3 years ago

292bf34d

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

ocfnash committed 3 years ago

fa204820

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

ocfnash committed 3 years ago

247504c8

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

ocfnash committed 3 years ago

a2fd0bd5

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

vihdzp committed 3 years ago

2e7efe99

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

Vierkantor committed 3 years ago

a7415855

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

ocfnash committed 3 years ago

c3273aa2

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

adamtopaz committed 3 years ago

3c00e5d7

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

YaelDillies committed 3 years ago

5b3cd4a9

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

YaelDillies committed 3 years ago

aaaeeaed

chore(*): update to lean 3.39.0c (#11821)

gebner committed 3 years ago

cedcf073

feat(group_theory/subgroup/basic): add pi subgroups (#11801)

nomeata committed 3 years ago

049a1b2b

feat(logic/basic): add projection notation for iff (#11803)

fpvandoorn committed 3 years ago

46c48d7f

fix(algebra/category/Module/colimits): Add some additional instances with permuted universe parameters (#11812)

adamtopaz committed 3 years ago

553cb9cc

chore(*): use le_rfl instead of le_refl _ (#11797)

jcommelin committed 3 years ago

4cfc30e3

feat(linear_algebra/lagrange): Add recurrence formula for Lagrange polynomials (#11762)

shingtaklam1324 committed 3 years ago

6dcad021