leanprover-community/mathlib

Pull Requests Commits

awainverse committed 3 years ago

19c3e1d9

Merge remote-tracking branch 'origin/fo_fg' into fraisse_limit

awainverse committed 3 years ago

0755575b

awainverse committed 3 years ago

67a0e9ec

Merge remote-tracking branch 'origin/fo_direct_limit' into fraisse_limit

awainverse committed 3 years ago

62ea7891

awainverse committed 3 years ago

e0bffed2

awainverse committed 3 years ago

658a069a

awainverse committed 3 years ago

8ea31806

Merge remote-tracking branch 'origin/split_up_model_theory' into fo_direct_limit

awainverse committed 3 years ago

790f84db

awainverse committed 3 years ago

ac4cae28

awainverse committed 3 years ago

164820fe

awainverse committed 3 years ago

bed7bafe

awainverse committed 3 years ago

4dd24462

awainverse committed 3 years ago

8fc15032

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

Older