leanprover-community/mathlib

Pull Requests Commits

dupuisf committed 3 years ago

2f179278

dupuisf committed 3 years ago

86d2e93c

Update src/algebra/star/self_adjoint.lean

dupuisf committed 3 years ago

Verified a0be2b3e

Merge branch 'master' into dupuisf/semilinear-paper-star-normal

dupuisf committed 3 years ago

3e9d8481

feat(topology/metric_space/basic): ext lemmas for metric spaces (#12070)

sgouezel committed 3 years ago

7dae87fe

feat(analysis/specific_limits): useful specializations of some lemmas (#12069)

sgouezel committed 3 years ago

5db1ae4c

feat(data/equiv/{basic,mul_equiv)}: add Pi_subsingleton (#12040)

nomeata committed 3 years ago

1bf41817

feat(field_theory/is_alg_closed): alg closed and char p implies perfect (#12037)

robertylewis committed 3 years ago

b2aaece0

feat(algebra/char_p/basic): add ring_char_of_prime_eq_zero (#12024)

Jlh18 committed 3 years ago

bd67e852

feat(data/part): Instance lemmas (#12001)

BoltonBailey committed 3 years ago

0fe91d0d

chore(data/finsupp/pointwise): golf using injective lemmas (#12086)

eric-wieser committed 3 years ago

b395a671

chore(topology/continuous_function/bounded): golf algebra instances (#12082)

eric-wieser committed 3 years ago

0ab9b5f3

chore(ring_theory/fractional_ideal): golf (#12076)

eric-wieser committed 3 years ago

d86ce027

feat(logic/basic): Better congruence lemmas for `or`, `or_or_or_comm` (#12004)

YaelDillies committed 3 years ago

15c6eee7

feat(category_theory/category/PartialFun): The category of types with partial functions (#11866)

YaelDillies committed 3 years ago

5e3d465c

docs(group_theory/semidirect_product): fix typo in module docs (#12083)

nomeata committed 3 years ago

3c78d00a

feat(algebra/char_p/basic): Generalize `frobenius_inj`. (#12079)

adamtopaz committed 3 years ago

3107a831

feat(data/finset/basic): When `insert` is injective and other lemmas (#11982)

YaelDillies committed 3 years ago

0eb160a5

feat(order/antisymmetrization): Turning a preorder into a partial order (#11728)

YaelDillies committed 3 years ago

6bcb12c1

chore(topology/algebra/mul_action): rename type variables (#12020)

urkud committed 3 years ago

8a286af6

chore(topology/algebra/module/basic): remove two duplicate lemmas (#12072)

eric-wieser committed 3 years ago

e8156757

feat(mv_polynomial/supported): restrict_to_vars (#12043)

robertylewis committed 3 years ago

a26d17fc

feat(analysis/complex/cauchy_integral, analysis/analytic/basic): entire functions have power series with infinite radius of convergence (#11948)

j-loreaux committed 3 years ago

62297cf0

chore(linear_algebra/affine_space/affine_map,topology/algebra/continuous_affine_map): generalized scalar instances (#11978)

eric-wieser committed 3 years ago

22fdf47e

feat(algebra/order/monoid): add simp lemmas (#12030)

mariainesdff committed 3 years ago

32beebbc

refactor(algebra/group/basic): add extra typeclasses for negation (#11960)

eric-wieser committed 3 years ago

75421198

feat(model_theory/terms_and_formulas): Define satisfiability and semantic equivalence of formulas (#11928)

awainverse committed 3 years ago

d24792c6

feat(algebra/star/self_adjoint): define skew-adjoint elements of a star additive group (#12013)

dupuisf committed 3 years ago

6dfb24cf

feat(analysis/special_functions/trigonometric/angle): `coe_pi_add_coe_pi` (#12064)

jsm28 committed 3 years ago

06e6b35d

feat(algebra/big_operators): formula for product of sums to n+1 (#12042)

robertylewis committed 3 years ago

daf2989a

Older