Commits leanprover-community/mathlib3

Merge branch 'master' into adomani_s_and_sos

adomani committed 4 years ago

e15c9258

feat(linear_algebra/eigenspace): generalized eigenvalues are just eigenvalues (#7059)

ocfnash committed 4 years ago

6ea4e9b1

feat(data/basic/lean): add lemmas finset.subset_iff_inter_eq_{left, right} (#7053)

adomani committed 4 years ago

9b4f0cf8

doc(undergrad.yaml): add equiv.perm.trunc_swap_factors (#7021)

eric-wieser committed 4 years ago

6a9bf98b

feat(group_theory/perm/cycles): Applying cycle_of to an is_cycle (#7000)

tb65536 committed 4 years ago

aa5ec528

feat(linear_algebra/free_module): a set of linearly independent vectors over a ring S is also linearly independent over a subring R of S (#6993)

adomani committed 4 years ago

ae6d77ba

feat(algebra/group/conj): `is_conj` for `monoid`s, `is_conj.setoid`, and `conj_classes` (#6896)

awainverse committed 4 years ago

5f0dbf65

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