leanprover-community/mathlib3

Pull Requests Commits

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

adomani committed 3 years ago

8a5f5c71

Merge branch 'adomani_ama_degree' of ssh://github.com/leanprover-community/mathlib into adomani_ama_degree

adomani committed 3 years ago

9c1f768f

partial reversion

adomani committed 3 years ago

2ff7ed13

Eric's version, inlining the definition of `degree`

adomani committed 3 years ago

Verified 4fc7edef

more general degree

adomani committed 3 years ago

37cdfae9

adomani committed 3 years ago

fea6a863

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

adomani committed 3 years ago

f2dbb653

adomani committed 3 years ago

2c28a19d

Eric's suggestion

adomani committed 3 years ago

Verified 0aabcfec

correct mistakes

adomani committed 3 years ago

775f4cb7

adomani committed 3 years ago

974d81b4

trailing_degree

adomani committed 3 years ago

1fb12c73

Revert "Eric's more general version"

adomani committed 3 years ago

7c770aa5

adomani committed 3 years ago

80c61ea1

Eric's more general version

adomani committed 3 years ago

f9ba6dad

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

degrees of add_monoid_algebras

adomani committed 3 years ago

612f3855

Newer Older