Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-04 19:03 d4ee5b69

View on Github →

fix(order.basic|ring_theory.algebra): lower instance priority (#1729)

  • algebra
  • algebra2
  • algebra3
  • algebra4
  • order.basic
  • module
  • algebra/ring
  • explain default priority of 100
  • undo priority changes

Estimated changes

added theorem gsmul_eq_smul
added theorem algebra.smul_def''
modified theorem algebra.smul_def
added theorem subalgebra.range_le