Commits leanprover-community/mathlib3

feat(data/fin/vec_notation): add `matrix.vec_map`

eric-wieser committed 3 years ago

6220fdfb

feat(topology/algebra/continuous_monoid_hom): New file (#11304)

tb65536 committed 3 years ago

912c47d3

feat(analysis/complex/basic): determinant of `conj_lie` (#11389)

jsm28 committed 3 years ago

c1f3f1af

chore(algebra/ring/basic): generalize `is_domain.to_cancel_monoid_with_zero` to `no_zero_divisors` (#11387)

eric-wieser committed 3 years ago

72c86c3f

feat(algebra/order/floor): adds some missing floor API (#11336)

b-mehta committed 3 years ago

cb1b6d97

feat(data/multiset/basic): add map_count_true_eq_filter_card (#11306)

BoltonBailey committed 3 years ago

bfe95158

chore(order/lexicographic): cleanup (#11299)

eric-wieser committed 3 years ago

9fd03e1d

feat(topology/uniform_space/compact_convergence): when the domain is locally compact, compact convergence is just locally uniform convergence (#11292)

ocfnash committed 3 years ago

deac58aa

feat(topology/homotopy/product): Product of homotopic paths (#11153)

prakol16 committed 3 years ago

20997252

feat(data/polynomial/taylor): taylor's formula (#11139)

pechersky committed 3 years ago

15b5e24e

feat(analysis/normed_space/lp_space): API for `lp.single` (#11307)

hrmacbeth committed 3 years ago

af074c84

refactor(topology/algebra/uniform_group): Use `to_additive` (#11366)

tb65536 committed 3 years ago

cdd44cd7

feat(analysis/special_functions/pow): norm_num extension for rpow (#11382)

digama0 committed 3 years ago

89f4786e

feat(data/nat/factorization): add lemma `factorization_le_iff_dvd` (#11377)

stuart-presnell committed 3 years ago

647598bd

fix(algebra/tropical/basic): provide explicit min and max (#11380)

eric-wieser committed 3 years ago

a5f79090

feat(algebra/indicator_function): add primed version for `mul_indicator_mul` and `indicator_sub` (#11379)

kex-y committed 3 years ago

73847ff3

feat(data/real/ennreal): add ennreal lemma for `a / 3 + a / 3 + a / 3 = a` (#11378)

kex-y committed 3 years ago

d1c49616

feat(group_theory/free_group): promote free_group_congr to a mul_equiv (#11373)

eric-wieser committed 3 years ago

57a8933b

feat(combinatorics/double_counting): Double-counting the edges of a bipartite graph (#11372)

YaelDillies committed 3 years ago

8db96a8f

feat(ring_theory/witt_vector): Witt vectors over a domain are a domain (#11346)

robertylewis committed 3 years ago

93e77412

feat(analysis/complex/isometry): `rotation` matrix representation and determinant (#11339)

jsm28 committed 3 years ago

83b03557

feat(data/complex/module,data/complex/determinant): `conj_ae` matrix representation and determinant (#11337)

jsm28 committed 3 years ago

e4a41e6f

feat(algebra/*): injective hom into kernel `map_eq_*_iff` (#11275)

pechersky committed 3 years ago

aa7a439d

feat(order/minimal): Subset of minimal/maximal elements (#11268)

YaelDillies committed 3 years ago

94fd004d

feat(data/polynomial/degree/lemmas): add induction principle for non-constant polynomials (#8463)

adomani committed 3 years ago

490847ee

chore(*): update to 3.38.0c (#11371)

gebner committed 3 years ago

b7107717

refactor(ring_theory/discriminant): refactor discr_not_zero_of_linear_independent (#11370)

riccardobrasca committed 3 years ago

b8d2affd

chore(set_theory/ordinal_arithmetic): Golfed some proofs (#11369)

vihdzp committed 3 years ago

380e28e9

feat(analysis/asymptotics/asymptotics): add `is_bounded_under.is_O_const` (#11367)

urkud committed 3 years ago

2963d7ce

refactor(topology/connected): drop `local attribute [instance] connected_component_setoid` (#11365)

urkud committed 3 years ago

8f5303ae