Commits leanprover-community/mathlib

feat(data/matrix): add matrix.fin_eta

eric-wieser committed 3 years ago

cd8c11ff

feat(measure_theory/constructions/prod): The layercake integral. (#14424)

kkytola committed 3 years ago

f3ae2d0d

feat(ring_theory): Basic framework for classes of ring homomorphisms (#14966)

erdOne committed 3 years ago

073c3ace

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

leanprover-community-bot committed 3 years ago

e479bfbe

chore(set_theory/pgame): remove redundant `dsimp` (#15312)

vihdzp committed 3 years ago

b89df0ab

chore(data/matrix/block): lemmas about swapping blocks of matrices (#15298)

eric-wieser committed 3 years ago

4302cb7e

doc(set_theory/ordinal/cantor_normal_form): document most theorems (#15227)

vihdzp committed 3 years ago

5590b0a2

chore(order/order_iso_nat): remove `decidable_pred` assumption from `subtype.order_iso_of_nat` (#15190)

vihdzp committed 3 years ago

5744b50d

feat(data/finset/basic): Add `decidable_nonempty` for finsets. (#15170)

linesthatinterlace committed 3 years ago

08648056

feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542)

Michael14071407 committed 3 years ago

1e82f5ec

feat(topology/local_homeomorph): "injectivity" local_homeomorph.prod (#15311)

fpvandoorn committed 3 years ago

f7313156

feat(analysis/calculus/cont_diff): extra lemmas about cont_diff_within_at (#15309)

fpvandoorn committed 3 years ago

25f60b46

feat(tactic/linear_combination): add parser for `h / a` (#15284)

digama0 committed 3 years ago

51f76d05

feat(topology/algebra/order): ⁻¹ continuous for linear ordered fields (#15022)

ericrbg committed 3 years ago

be53c7cb

feat(combinatorics/additive/behrend): Behrend's construction (#14070)

YaelDillies committed 3 years ago

44999a92

feat(set_theory/ordinal/basic): mark `type_fintype` as `simp` (#15194)

vihdzp committed 3 years ago

2084baf2

refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` (#15191)

eric-wieser committed 3 years ago

93e164e8

chore(*/enat): rename files (#15245)

urkud committed 3 years ago

ed5453cd

fix(algebra/group/units): splitting out `mul_one_class` for group of units (#14923)

eric-wieser committed 3 years ago

f8488beb

feat(algebra/order/complete_field): `conditionally_complete_linear_ordered_field`, aka the reals (#3292)

alexjbest committed 3 years ago

632b0312

chore(analysis/inner_product_space): move definition of self-adjointness (#15281)

mcdoll committed 3 years ago

1d048c57

feat(ring_theory/rees_algebra): Define the Rees algebra of an ideal. (#15089)

erdOne committed 3 years ago

2dfa69c1

feat(measure_theory/pmf): lawful monad instance for probability mass function monad (#15066)

dtumad committed 3 years ago

8d7f0012

feat(data/matrix/notation): add `!![1, 2; 3, 4]` notation (#14991)

eric-wieser committed 3 years ago

83092fb4

feat(data/polynomial/unit_trinomial): An irreducibility criterion for unit trinomials (#14914)

tb65536 committed 3 years ago

01a18244

feat(data/polynomial/erase_lead): Characterization of polynomials of fixed support (#14741)

tb65536 committed 3 years ago

581b6940

feat(information_theory/hamming): add Hamming distance and norm (#14739)

linesthatinterlace committed 3 years ago

73402033

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

leanprover-community-bot committed 3 years ago

b06e32c2

refactor(logic/is_empty): tag `is_empty.forall_iff` and `is_empty.exists_iff` as `simp` (#14660)

vihdzp committed 3 years ago

5cb17dd1

refactor(topology/subset_properties): reformulate `is_clopen_b{Union,Inter}` in terms of `set.finite` (#15272)

urkud committed 3 years ago

ea13c1cf