Untitled Diff
1 लाइन
@eq.{u_1+1} (fin (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)) → L) (@matrix.vec_cons.{u_1} L (@has_one.one.{0} nat nat.has_one) (@has_one.one.{u_1} L (@monoid.to_has_one.{u_1} L (@ring.to_monoid.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))) (@matrix.vec_cons.{u_1} L (@has_zero.zero.{0} nat nat.has_zero) (@has_zero.zero.{u_1} L (@mul_zero_class.to_has_zero.{u_1} L (@monoid_with_zero.to_mul_zero_class.{u_1} L (@semiring.to_monoid_with_zero.{u_1} L (@ring.to_semiring.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))))) (@matrix.vec_empty.{u_1} L))) (@has_zero.zero.{u_1} (fin (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)) → L) (@add_monoid.to_has_zero.{u_1} (fin (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)) → L) (@add_group.to_add_monoid.{u_1} (fin (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)) → L) (@add_comm_group.to_add_group.{u_1} (fin (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)) → L) (@pi.add_comm_group.{0 u_1} (fin (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one))) (λ (ᾰ : fin (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one))), L) (λ (i : fin (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one))), @ring.to_add_comm_group.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))))))
@eq.{(max 1 (u_1+1))} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@matrix.vec_cons.{u_1} L (nat.succ (@has_zero.zero.{0} nat nat.has_zero)) (@has_one.one.{u_1} L (@monoid.to_has_one.{u_1} L (@ring.to_monoid.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))) (@matrix.vec_cons.{u_1} L (@has_zero.zero.{0} nat nat.has_zero) (@has_zero.zero.{u_1} L (@mul_zero_class.to_has_zero.{u_1} L (@monoid_with_zero.to_mul_zero_class.{u_1} L (@semiring.to_monoid_with_zero.{u_1} L (@ring.to_semiring.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))))) (@matrix.vec_empty.{u_1} L))) (@has_zero.zero.{u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@pi.has_zero.{0 u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))) (λ (ᾰ : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), L) (λ (i : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), @mul_zero_class.to_has_zero.{u_1} L (@monoid_with_zero.to_mul_zero_class.{u_1} L (@semiring.to_monoid_with_zero.{u_1} L (@ring.to_semiring.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))))))