Commits leanprover-community/mathlib3

feat(algebra/add_submonoid_closure): the additive closure of a multiplicative submonoid is a subsemiring (#6860)

adomani committed 4 years ago

41137fe0

feat(topology/continuous_function): lemmas about coe (#7055)

kim-em committed 4 years ago

5254ef14

feat(algebra/pointwise): improve instances on `set_semiring` (#7050)

eric-wieser committed 4 years ago

43aee091

feat(algebra/lie/subalgebra): define the restriction of a Lie module to a Lie subalgebra (#7036)

ocfnash committed 4 years ago

7928ca07

refactor(algebra/group/inj_surj): eliminate the versions of the definitions without `has_div` / `has_sub`. (#7035)

eric-wieser committed 4 years ago

2b7b1e72

feat(topology/constructions): `function.update` is continuous in both arguments (#7023)

urkud committed 4 years ago

0007c4a2

feat(data/finsupp,linear_algebra/finsupp): `finsupp`s and sum types (#6992)

Vierkantor committed 4 years ago

d7f6bd61

refactor(analysis/normed_space/normed_group_hom): generalize to semi_normed_group (#6977)

riccardobrasca committed 4 years ago

82b0b30e

feat(group_theory/perm/*): facts about the cardinality of the support of a permutation (#6951)

awainverse committed 4 years ago

02058ed7

feat(algebra/category/Module): compare concrete and abstract kernels (#6938)

kim-em committed 4 years ago

07aa34e7

feat(category_theory): Type u is well-powered (#6812)

kim-em committed 4 years ago

3a99001a

chore(scripts): update nolints.txt (#7052)

leanprover-community-bot committed 4 years ago

2daf2ff5

chore(data/finsupp/pointwise): add missing `finsupp.mul_zero_class` (#7049)

ocfnash committed 4 years ago

6f38c145

feat(linear_algebra/finsupp): add refl/trans/symm lemmas for dom_lcongr (#7048)

eric-wieser committed 4 years ago

aa665b12

feat(order/complete_lattice): le_Sup and Inf_le iff lemmas (#7047)

b-mehta committed 4 years ago

8b34e00d

chore(group_theory/group_action): cleanup (#7045)

dwarn committed 4 years ago

ba264c4f

chore(group_theory/order_of_element): move some lemmas (#7031)

Julian-Kuelshammer committed 4 years ago

53128954

feat(measure_theory/interval_integral): more on integral_comp (#7030)

benjamindavidson committed 4 years ago

dbb2b558

feat(logic/girard): Girard's paradox (#7026)

digama0 committed 4 years ago

82fd6e1e

feat(linear_algebra): `c ≤ dim K E` iff there exists a linear independent `s : set E`, `card s = c` (#7014)

urkud committed 4 years ago

415b369d

chore(data/fintype/basic): add `card_unique` and a warning note to `card_of_subsingleton` (#7008)

eric-wieser committed 4 years ago

4192612b

chore(topology/continuous_function/algebra): add simp lemmas for smul coercion, move names out of global namespace (#7007)

ocfnash committed 4 years ago

975f5333

feat(algebra/category): the category of R-modules is well-powered (#7002)

TwoFX committed 4 years ago

90e265ea

feat(group_theory/perm/sign): Order of product of disjoint permutations (#6998)

tb65536 committed 4 years ago

030a7047

feat(category_theory): equivalences preserve epis and monos (#6994)

TwoFX committed 4 years ago

fe16235f

feat(archive/imo): formalize IMO 2005 Q3 (#6984)

manuelcandales committed 4 years ago

89ea423d

chore(group_theory/subgroup): translate map comap lemmas from linear_map (#6979)

AdrianDoM committed 4 years ago

b05affbd

feat(category_theory/preadditive): additive functors preserve biproducts (#6882)

kim-em committed 4 years ago

6aa0e30e

refactor(topology/sheaves): Refactor sheaf condition proofs (#6962)

justus-springer committed 4 years ago

4ddbdc1b

feat(archive/imo): formalize IMO 2008 Q2 (#6958)

manuelcandales committed 4 years ago

1e1eaae6