Commits leanprover-community/mathlib3

Update adjugate.lean

eric-wieser committed 3 years ago

Verified e038ce30

feat(data/matrix/basic): promote subsingleton instances to unique instances

eric-wieser committed 3 years ago

d5c2cdaf

feat(linear_algebra/clifford_algebra/even): Universal property and isomorphisms for the even subalgebra (#14790)

eric-wieser committed 3 years ago

56199b7b

refactor(linear_algebra, analysis/inner_product_space): use `⊤ ≤` instead of `= ⊤` in bases constructors (#15697)

ADedecker committed 3 years ago

6b647c3b

feat(analysis/normed_space/compact_operator): definition and basic facts about compact operators (#15467)

ADedecker committed 3 years ago

4ff8c3db

feat(probability/strong_law): Lp version of the strong law of large numbers (#15392)

kex-y committed 3 years ago

b33d6d6e

fix(tactic/polyrith): remove unnecessary 1* from polyrith output (#15292)

robertylewis committed 3 years ago

5fc18b5e

feat(data/{pi, prod}): add missing `has_pow` instances for `pi` type (#15478)

jjaassoonn committed 3 years ago

39046bda

feat(algebra/module): sub_mem_sup for modules over rings (#15733)

alexjbest committed 3 years ago

8b87d337

feat(data/pi/algebra): sum_elim lemmas (#15588)

abentkamp committed 3 years ago

1065169f

feat(test/polyrith): better formatting for generated tests (#15728)

robertylewis committed 3 years ago

94dcadd5

chore(field_theory/splitting_field): remove unneeded parameter (#15716)

Vierkantor committed 3 years ago

123f4542

feat(group_theory/finite_abelian): a finitely generated torsion abelian group is finite (#15402)

Multramate committed 3 years ago

adeda57b

chore(measure_theory/tactic): remove the measurability attribute from two lemmas (#15295)

RemyDegenne committed 3 years ago

71d01152

feat(order/bounded_order): `is_well_order` instances for `with_top` and `with_bot` (#15278)

vihdzp committed 3 years ago

af213089

chore(category_theory/adjunction): fix a typo (#15720)

TwoFX committed 3 years ago

d3b1dbee

chore(topology/algebra/module, analysis/normed_space/linear_isometry): dedup `submodule.subtypeL` and `continuous_linear_map.subtype_val` (#15700)

ADedecker committed 3 years ago

cad19073

feat(category_theory): construction of the localized category (#14422)

joelriou committed 3 years ago

350a3817

feat(category_theory/limits/shapes/comm_sq): opposites of is_pullback and is_pushout (#15269)

joelriou committed 3 years ago

00e7ca52

feat(topology/subset_properties): `locally_compact_space` instance for `Π` types (#15707)

ralvrz committed 3 years ago

cd7b23d1

feat(algebraic_geometry/morphisms): Quasi-compact morphisms of schemes (#15436)

erdOne committed 3 years ago

805bb2d2

feat(combinatorics/additive/behrend): Behrend's lower bound on Roth numbers (#15327)

YaelDillies committed 3 years ago

594e8848

feat(analysis/special_functions/gaussian): formula for gaussian integrals (#15106)

sgouezel committed 3 years ago

732279dd

feat(probability/martingale): the discrete stochastic integral of a submartingale is a submartingale (#14909)

kex-y committed 3 years ago

3086d342

feat(category_theory): a characterization of separating objects (#14838)

TwoFX committed 3 years ago

583a7034

chore(data/polynomial/cancel_leads): golf using `compute_degree_le` (#14776)

adomani committed 3 years ago

08af4a31

chore(analysis/convex/cone): add trivial coercion lemmas (#15713)

eric-wieser committed 3 years ago

c59720b4

feat(analysis/special_functions/trigonometric/angle): equality of `cos` or `sin` (#15651)

jsm28 committed 3 years ago

63eb48be

doc(field_theory/splitting_field): update code example to reflect changes to diamond issues (#15620)

eric-wieser committed 3 years ago

45732987

feat(linear_algebra): lemmas on associatedness of determinants of linear maps (#15587)

Vierkantor committed 3 years ago

ac2addd1